Home | Metamath
Proof Explorer Theorem List (p. 85 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pmex 8401* | The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ (Fun 𝑓 ∧ 𝑓 ⊆ (𝐴 × 𝐵))} ∈ V) | ||
Theorem | mapex 8402* | The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V) | ||
Theorem | fnmap 8403 | Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ↑m Fn (V × V) | ||
Theorem | fnpm 8404 | Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ ↑pm Fn (V × V) | ||
Theorem | reldmmap 8405 | Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.) |
⊢ Rel dom ↑m | ||
Theorem | mapvalg 8406* | The value of set exponentiation. (𝐴 ↑m 𝐵) is the set of all functions that map from 𝐵 to 𝐴. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑m 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴}) | ||
Theorem | pmvalg 8407* | The value of the partial mapping operation. (𝐴 ↑pm 𝐵) is the set of all partial functions that map from 𝐵 to 𝐴. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 ↑pm 𝐵) = {𝑓 ∈ 𝒫 (𝐵 × 𝐴) ∣ Fun 𝑓}) | ||
Theorem | mapval 8408* | The value of set exponentiation (inference version). (𝐴 ↑m 𝐵) is the set of all functions that map from 𝐵 to 𝐴. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m 𝐵) = {𝑓 ∣ 𝑓:𝐵⟶𝐴} | ||
Theorem | elmapg 8409 | Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | ||
Theorem | elmapd 8410 | Deduction form of elmapg 8409. (Contributed by BJ, 11-Apr-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴)) | ||
Theorem | mapdm0 8411 | The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux, 3-Dec-2021.) |
⊢ (𝐵 ∈ 𝑉 → (𝐵 ↑m ∅) = {∅}) | ||
Theorem | elpmg 8412 | The predicate "is a partial function." (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐶 ∧ 𝐶 ⊆ (𝐵 × 𝐴)))) | ||
Theorem | elpm2g 8413 | The predicate "is a partial function." (Contributed by NM, 31-Dec-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))) | ||
Theorem | elpm2r 8414 | Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐹:𝐶⟶𝐴 ∧ 𝐶 ⊆ 𝐵)) → 𝐹 ∈ (𝐴 ↑pm 𝐵)) | ||
Theorem | elpmi 8415 | A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) | ||
Theorem | pmfun 8416 | A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → Fun 𝐹) | ||
Theorem | elmapex 8417 | Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V)) | ||
Theorem | elmapi 8418 | A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵) | ||
Theorem | elmapfn 8419 | A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶) | ||
Theorem | elmapfun 8420 | A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → Fun 𝐴) | ||
Theorem | elmapssres 8421 | A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷)) | ||
Theorem | fpmg 8422 | A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | pmss12g 8423 | Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷)) | ||
Theorem | pmresg 8424 | Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) | ||
Theorem | elmap 8425 | Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴) | ||
Theorem | mapval2 8426* | Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵}) | ||
Theorem | elpm 8427 | The predicate "is a partial function." (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (𝐵 × 𝐴))) | ||
Theorem | elpm2 8428 | The predicate "is a partial function." (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) | ||
Theorem | fpm 8429 | A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | mapsspm 8430 | Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝐴 ↑m 𝐵) ⊆ (𝐴 ↑pm 𝐵) | ||
Theorem | pmsspw 8431 | Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ↑pm 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) | ||
Theorem | mapsspw 8432 | Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ↑m 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) | ||
Theorem | mapfvd 8433 | The value of a function that maps from 𝐵 to 𝐴. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝑀 = (𝐴 ↑m 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | elmapresaun 8434 | fresaun 6543 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵))) | ||
Theorem | fvmptmap 8435* | Special case of fvmpt 6762 for operator theorems. (Contributed by NM, 27-Nov-2007.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑅 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑m 𝐷) ↦ 𝐵) ⇒ ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | map0e 8436 | Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 14-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑m ∅) = 1o) | ||
Theorem | map0b 8437 | Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≠ ∅ → (∅ ↑m 𝐴) = ∅) | ||
Theorem | map0g 8438 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅))) | ||
Theorem | mapsnd 8439* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}}) | ||
Theorem | map0 8440 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅)) | ||
Theorem | mapsn 8441* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}} | ||
Theorem | mapss 8442 | Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) | ||
Theorem | fdiagfn 8443* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) | ||
Theorem | fvdiagfn 8444* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋})) | ||
Theorem | mapsnconst 8445 | Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐵 ↑m 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)})) | ||
Theorem | mapsncnv 8446* | Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) | ||
Theorem | mapsnf1o2 8447* | Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ 𝐹:(𝐵 ↑m 𝑆)–1-1-onto→𝐵 | ||
Theorem | mapsnf1o3 8448* | Explicit bijection in the reverse of mapsnf1o2 8447. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) ⇒ ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑m 𝑆) | ||
Theorem | ralxpmap 8449* | Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓)) | ||
Syntax | cixp 8450 | Extend class notation to include infinite Cartesian products. |
class X𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-ixp 8451* | Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥 ∈ 𝐴 written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.) |
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | ||
Theorem | dfixp 8452* | Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 8451, under the assumption that 𝐴 and 𝑥 are disjoint. This way, we can say that 𝑥 is bound in X𝑥 ∈ 𝐴𝐵 even if it appears free in 𝐴. (Contributed by Mario Carneiro, 12-Aug-2016.) |
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | ||
Theorem | ixpsnval 8453* | The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.) |
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)}) | ||
Theorem | elixp2 8454* | Membership in an infinite Cartesian product. See df-ixp 8451 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | fvixp 8455* | Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷) | ||
Theorem | ixpfn 8456* | A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴) | ||
Theorem | elixp 8457* | Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | elixpconst 8458* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | ixpconstg 8459* | Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴)) | ||
Theorem | ixpconst 8460* | Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴) | ||
Theorem | ixpeq1 8461* | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ixpeq1d 8462* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ss2ixp 8463 | Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2 8464 | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2dva 8465* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2dv 8466* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | cbvixp 8467* | Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbvixpv 8468* | Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 | ||
Theorem | nfixpw 8469* | Version of nfixp 8470 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfixp 8470 | Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfixp1 8471 | The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | ixpprc 8472* | A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain 𝐴, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.) |
⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 = ∅) | ||
Theorem | ixpf 8473* | A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹:𝐴⟶∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | uniixp 8474* | The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | ixpexg 8475* | The existence of an infinite Cartesian product. 𝑥 is normally a free-variable parameter in 𝐵. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 25-Jan-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | ixpin 8476* | The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpiin 8477* | The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) |
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpint 8478* | The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦) | ||
Theorem | ixp0x 8479 | An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.) |
⊢ X𝑥 ∈ ∅ 𝐴 = {∅} | ||
Theorem | ixpssmap2g 8480* | An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 8481 avoids ax-rep 5182. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)) | ||
Theorem | ixpssmapg 8481* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)) | ||
Theorem | 0elixp 8482 | Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.) |
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴 | ||
Theorem | ixpn0 8483 | The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 9894. (Contributed by Mario Carneiro, 22-Jun-2016.) |
⊢ (X𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀𝑥 ∈ 𝐴 𝐵 ≠ ∅) | ||
Theorem | ixp0 8484 | The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 9894. (Contributed by NM, 1-Oct-2006.) (Proof shortened by Mario Carneiro, 22-Jun-2016.) |
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅) | ||
Theorem | ixpssmap 8485* | An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴) | ||
Theorem | resixp 8486* | Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐶) → (𝐹 ↾ 𝐵) ∈ X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | undifixp 8487* | Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.) |
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | mptelixpg 8488* | Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.) |
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)) | ||
Theorem | resixpfo 8489* | Restriction of elements of an infinite Cartesian product creates a surjection, if the original Cartesian product is nonempty. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝐹 = (𝑓 ∈ X𝑥 ∈ 𝐴 𝐶 ↦ (𝑓 ↾ 𝐵)) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ X𝑥 ∈ 𝐴 𝐶 ≠ ∅) → 𝐹:X𝑥 ∈ 𝐴 𝐶–onto→X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | elixpsn 8490* | Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) | ||
Theorem | ixpsnf1o 8491* | A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐹:𝐴–1-1-onto→X𝑦 ∈ {𝐼}𝐴) | ||
Theorem | mapsnf1o 8492* | A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑m {𝐼})) | ||
Theorem | boxriin 8493* | A rectangular subset of a rectangular set can be recovered as the relative intersection of single-axis restrictions. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (∀𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → X𝑥 ∈ 𝐼 𝐴 = (X𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐴, 𝐵))) | ||
Theorem | boxcutc 8494* | The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) = X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)) | ||
Syntax | cen 8495 | Extend class definition to include the equinumerosity relation ("approximately equals" symbol) |
class ≈ | ||
Syntax | cdom 8496 | Extend class definition to include the dominance relation (curly "less than or equal to") |
class ≼ | ||
Syntax | csdm 8497 | Extend class definition to include the strict dominance relation (curly less-than) |
class ≺ | ||
Syntax | cfn 8498 | Extend class definition to include the class of all finite sets. |
class Fin | ||
Definition | df-en 8499* | Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ≈ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 8507. (Contributed by NM, 28-Mar-1998.) |
⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} | ||
Definition | df-dom 8500* | Define the dominance relation. For an alternate definition see dfdom2 8524. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 8510 and domen 8511. (Contributed by NM, 28-Mar-1998.) |
⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |