Home | Metamath
Proof Explorer Theorem List (p. 80 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fdiagfn 7901* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼)) | ||
Theorem | fvdiagfn 7902* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋})) | ||
Theorem | mapsnconst 7903 | Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)})) | ||
Theorem | mapsncnv 7904* | 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 & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) | ||
Theorem | mapsnf1o2 7905* | Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ 𝐹:(𝐵 ↑𝑚 𝑆)–1-1-onto→𝐵 | ||
Theorem | mapsnf1o3 7906* | Explicit bijection in the reverse of mapsnf1o2 7905. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) ⇒ ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑𝑚 𝑆) | ||
Theorem | ralxpmap 7907* | 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.) |
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑𝑚 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑𝑚 (𝑇 ∖ {𝐽}))𝜓)) | ||
Syntax | cixp 7908 | Extend class notation to include infinite Cartesian products. |
class X𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-ixp 7909* | 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 7910* | Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 7909, 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 7911* | The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.) |
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)}) | ||
Theorem | elixp2 7912* | Membership in an infinite Cartesian product. See df-ixp 7909 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | fvixp 7913* | Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷) | ||
Theorem | ixpfn 7914* | A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴) | ||
Theorem | elixp 7915* | Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | elixpconst 7916* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | ixpconstg 7917* | Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴)) | ||
Theorem | ixpconst 7918* | Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴) | ||
Theorem | ixpeq1 7919* | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ixpeq1d 7920* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ss2ixp 7921 | Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2 7922 | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2dva 7923* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2dv 7924* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | cbvixp 7925* | Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbvixpv 7926* | Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 | ||
Theorem | nfixp 7927 | Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfixp1 7928 | 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 7929* | 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 7930* | 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 7931* | 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 7932* | 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 7933* | The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpiin 7934* | The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) |
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpint 7935* | The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦) | ||
Theorem | ixp0x 7936 | An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.) |
⊢ X𝑥 ∈ ∅ 𝐴 = {∅} | ||
Theorem | ixpssmap2g 7937* | An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 7938 avoids ax-rep 4771. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) | ||
Theorem | ixpssmapg 7938* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) | ||
Theorem | 0elixp 7939 | Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.) |
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴 | ||
Theorem | ixpn0 7940 | 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 9305. (Contributed by Mario Carneiro, 22-Jun-2016.) |
⊢ (X𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀𝑥 ∈ 𝐴 𝐵 ≠ ∅) | ||
Theorem | ixp0 7941 | 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 9305. (Contributed by NM, 1-Oct-2006.) (Proof shortened by Mario Carneiro, 22-Jun-2016.) |
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅) | ||
Theorem | ixpssmap 7942* | An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴) | ||
Theorem | resixp 7943* | 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 7944* | Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.) |
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | mptelixpg 7945* | Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.) |
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)) | ||
Theorem | resixpfo 7946* | 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 7947* | Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) | ||
Theorem | ixpsnf1o 7948* | 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 7949* | A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑𝑚 {𝐼})) | ||
Theorem | boxriin 7950* | 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 7951* | 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 7952 | Extend class definition to include the equinumerosity relation ("approximately equals" symbol) |
class ≈ | ||
Syntax | cdom 7953 | Extend class definition to include the dominance relation (curly less-than-or-equal) |
class ≼ | ||
Syntax | csdm 7954 | Extend class definition to include the strict dominance relation (curly less-than) |
class ≺ | ||
Syntax | cfn 7955 | Extend class definition to include the class of all finite sets. |
class Fin | ||
Definition | df-en 7956* | 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 7964. (Contributed by NM, 28-Mar-1998.) |
⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} | ||
Definition | df-dom 7957* | Define the dominance relation. For an alternate definition see dfdom2 7981. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 7967 and domen 7968. (Contributed by NM, 28-Mar-1998.) |
⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | ||
Definition | df-sdom 7958 | Define the strict dominance relation. Alternate possible definitions are derived as brsdom 7978 and brsdom2 8084. Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.) |
⊢ ≺ = ( ≼ ∖ ≈ ) | ||
Definition | df-fin 7959* | Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 8538. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (theorem isfinite 8549.) (Contributed by NM, 22-Aug-2008.) |
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} | ||
Theorem | relen 7960 | Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.) |
⊢ Rel ≈ | ||
Theorem | reldom 7961 | Dominance is a relation. (Contributed by NM, 28-Mar-1998.) |
⊢ Rel ≼ | ||
Theorem | relsdom 7962 | Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.) |
⊢ Rel ≺ | ||
Theorem | encv 7963 | If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | bren 7964* | Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) |
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | ||
Theorem | brdomg 7965* | Dominance relation. (Contributed by NM, 15-Jun-1998.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) | ||
Theorem | brdomi 7966* | Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) | ||
Theorem | brdom 7967* | Dominance relation. (Contributed by NM, 15-Jun-1998.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) | ||
Theorem | domen 7968* | Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
Theorem | domeng 7969* | Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))) | ||
Theorem | ctex 7970 | A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) | ||
Theorem | f1oen3g 7971 | The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 7974 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
Theorem | f1oen2g 7972 | The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 7974 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
Theorem | f1dom2g 7973 | The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 7975 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
Theorem | f1oeng 7974 | The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
Theorem | f1domg 7975 | The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.) |
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)) | ||
Theorem | f1oen 7976 | The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵) | ||
Theorem | f1dom 7977 | The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵) | ||
Theorem | brsdom 7978 | Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴." Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.) |
⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | ||
Theorem | isfi 7979* | Express "𝐴 is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008.) |
⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) | ||
Theorem | enssdom 7980 | Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.) |
⊢ ≈ ⊆ ≼ | ||
Theorem | dfdom2 7981 | Alternate definition of dominance. (Contributed by NM, 17-Jun-1998.) |
⊢ ≼ = ( ≺ ∪ ≈ ) | ||
Theorem | endom 7982 | Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.) |
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) | ||
Theorem | sdomdom 7983 | Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.) |
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) | ||
Theorem | sdomnen 7984 | Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.) |
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) | ||
Theorem | brdom2 7985 | Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.) |
⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵)) | ||
Theorem | bren2 7986 | Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.) |
⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵)) | ||
Theorem | enrefg 7987 | Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) | ||
Theorem | enref 7988 | Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≈ 𝐴 | ||
Theorem | eqeng 7989 | Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) | ||
Theorem | domrefg 7990 | Dominance is reflexive. (Contributed by NM, 18-Jun-1998.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴) | ||
Theorem | en2d 7991* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ V)) & ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ V)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
Theorem | en3d 7992* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) |
⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))) ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
Theorem | en2i 7993* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)) ⇒ ⊢ 𝐴 ≈ 𝐵 | ||
Theorem | en3i 7994* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ 𝐴 ≈ 𝐵 | ||
Theorem | dom2lem 7995* | A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶):𝐴–1-1→𝐵) | ||
Theorem | dom2d 7996* | A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 20-May-2013.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝑅 → 𝐴 ≼ 𝐵)) | ||
Theorem | dom3d 7997* | A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by Mario Carneiro, 20-May-2013.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐴 ≼ 𝐵) | ||
Theorem | dom2 7998* | A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. 𝐶 and 𝐷 can be read 𝐶(𝑥) and 𝐷(𝑦), as can be inferred from their distinct variable conditions. (Contributed by NM, 26-Oct-2003.) |
⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)) ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐴 ≼ 𝐵) | ||
Theorem | dom3 7999* | A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. 𝐶 and 𝐷 can be read 𝐶(𝑥) and 𝐷(𝑦), as can be inferred from their distinct variable conditions. (Contributed by Mario Carneiro, 20-May-2013.) |
⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐶 = 𝐷 ↔ 𝑥 = 𝑦)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ 𝐵) | ||
Theorem | idssen 8000 | Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ I ⊆ ≈ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |