Home | Metamath
Proof Explorer Theorem List (p. 81 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 | ssdomg 8001 | A set dominates its subsets. Theorem 16 of [Suppes] p. 94. (Contributed by NM, 19-Jun-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 ⊆ 𝐵 → 𝐴 ≼ 𝐵)) | ||
Theorem | ener 8002 | Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) (Proof shortened by AV, 1-May-2021.) |
⊢ ≈ Er V | ||
Theorem | enerOLD 8003 | Obsolete proof of ener 8002 as of 1-May-2021. Equinumerosity is an equivalence relation. (Contributed by NM, 19-Mar-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ≈ Er V | ||
Theorem | ensymb 8004 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) | ||
Theorem | ensym 8005 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | ||
Theorem | ensymi 8006 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 | ||
Theorem | ensymd 8007 | Symmetry of equinumerosity. Deduction form of ensym 8005. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) | ||
Theorem | entr 8008 | Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
Theorem | domtr 8009 | Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | entri 8010 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 | ||
Theorem | entr2i 8011 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 | ||
Theorem | entr3i 8012 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 | ||
Theorem | entr4i 8013 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 | ||
Theorem | endomtr 8014 | Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | domentr 8015 | Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | f1imaeng 8016 | A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | f1imaen2g 8017 | A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen 8018 does not need ax-reg 8497.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | f1imaen 8018 | A one-to-one function's image under a subset of its domain is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | en0 8019 | The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) |
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | ||
Theorem | ensn1 8020 | A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1𝑜 | ||
Theorem | ensn1g 8021 | A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1𝑜) | ||
Theorem | enpr1g 8022 | {𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1𝑜) | ||
Theorem | en1 8023* | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.) |
⊢ (𝐴 ≈ 1𝑜 ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | en1b 8024 | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ (𝐴 ≈ 1𝑜 ↔ 𝐴 = {∪ 𝐴}) | ||
Theorem | reuen1 8025* | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1𝑜) | ||
Theorem | euen1 8026 | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1𝑜) | ||
Theorem | euen1b 8027* | Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐴 ≈ 1𝑜 ↔ ∃!𝑥 𝑥 ∈ 𝐴) | ||
Theorem | en1uniel 8028 | A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ (𝑆 ≈ 1𝑜 → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | 2dom 8029* | A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.) |
⊢ (2𝑜 ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) | ||
Theorem | fundmen 8030 | A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 28-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (Fun 𝐹 → dom 𝐹 ≈ 𝐹) | ||
Theorem | fundmeng 8031 | A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.) |
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) | ||
Theorem | cnven 8032 | A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) | ||
Theorem | cnvct 8033 | If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) | ||
Theorem | fndmeng 8034 | A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) | ||
Theorem | mapsnen 8035 | Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑𝑚 {𝐵}) ≈ 𝐴 | ||
Theorem | map1 8036 | Set exponentiation: ordinal 1 to any set is equinumerous to ordinal 1. Exercise 4.42(b) of [Mendelson] p. 255. (Contributed by NM, 17-Dec-2003.) |
⊢ (𝐴 ∈ 𝑉 → (1𝑜 ↑𝑚 𝐴) ≈ 1𝑜) | ||
Theorem | en2sn 8037 | Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) | ||
Theorem | snfi 8038 | A singleton is finite. (Contributed by NM, 4-Nov-2002.) |
⊢ {𝐴} ∈ Fin | ||
Theorem | fiprc 8039 | The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.) |
⊢ Fin ∉ V | ||
Theorem | unen 8040 | Equinumerosity of union of disjoint sets. Theorem 4 of [Suppes] p. 92. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) ∧ ((𝐴 ∩ 𝐶) = ∅ ∧ (𝐵 ∩ 𝐷) = ∅)) → (𝐴 ∪ 𝐶) ≈ (𝐵 ∪ 𝐷)) | ||
Theorem | ssct 8041 | Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) | ||
Theorem | difsnen 8042 | All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})) | ||
Theorem | domdifsn 8043 | Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ (𝐵 ∖ {𝐶})) | ||
Theorem | xpsnen 8044 | A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 4-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 × {𝐵}) ≈ 𝐴 | ||
Theorem | xpsneng 8045 | A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of [Mendelson] p. 254. (Contributed by NM, 22-Oct-2004.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × {𝐵}) ≈ 𝐴) | ||
Theorem | xp1en 8046 | One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1𝑜) ≈ 𝐴) | ||
Theorem | endisj 8047* | Any two sets are equinumerous to disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃𝑥∃𝑦((𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵) ∧ (𝑥 ∩ 𝑦) = ∅) | ||
Theorem | undom 8048 | Dominance law for union. Proposition 4.24(a) of [Mendelson] p. 257. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) | ||
Theorem | xpcomf1o 8049* | The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) | ||
Theorem | xpcomco 8050* | Composition with the bijection of xpcomf1o 8049 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) & ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | xpcomen 8051 | Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 5-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 × 𝐵) ≈ (𝐵 × 𝐴) | ||
Theorem | xpcomeng 8052 | Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) | ||
Theorem | xpsnen2g 8053 | A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵) | ||
Theorem | xpassen 8054 | Associative law for equinumerosity of Cartesian product. Proposition 4.22(e) of [Mendelson] p. 254. (Contributed by NM, 22-Jan-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 × 𝐵) × 𝐶) ≈ (𝐴 × (𝐵 × 𝐶)) | ||
Theorem | xpdom2 8055 | Dominance law for Cartesian product. Proposition 10.33(2) of [TakeutiZaring] p. 92. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) | ||
Theorem | xpdom2g 8056 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) | ||
Theorem | xpdom1g 8057 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 25-Mar-2006.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶)) | ||
Theorem | xpdom3 8058 | A set is dominated by its Cartesian product with a nonempty set. Exercise 6 of [Suppes] p. 98. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 × 𝐵)) | ||
Theorem | xpdom1 8059 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 28-Sep-2004.) (Revised by NM, 29-Mar-2006.) (Revised by Mario Carneiro, 7-May-2015.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 → (𝐴 × 𝐶) ≼ (𝐵 × 𝐶)) | ||
Theorem | domunsncan 8060 | A singleton cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌) → (({𝐴} ∪ 𝑋) ≼ ({𝐵} ∪ 𝑌) ↔ 𝑋 ≼ 𝑌)) | ||
Theorem | omxpenlem 8061* | Lemma for omxpen 8062. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·𝑜 𝐵)) | ||
Theorem | omxpen 8062 | The cardinal and ordinal products are always equinumerous. Exercise 10 of [TakeutiZaring] p. 89. (Contributed by Mario Carneiro, 3-Mar-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 𝐵) ≈ (𝐴 × 𝐵)) | ||
Theorem | omf1o 8063* | Construct an explicit bijection from 𝐴 ·𝑜 𝐵 to 𝐵 ·𝑜 𝐴. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·𝑜 𝑥) +𝑜 𝑦)) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐵 ·𝑜 𝑦) +𝑜 𝑥)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐺 ∘ ◡𝐹):(𝐴 ·𝑜 𝐵)–1-1-onto→(𝐵 ·𝑜 𝐴)) | ||
Theorem | pw2f1olem 8064* | Lemma for pw2f1o 8065. (Contributed by Mario Carneiro, 6-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑𝑚 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶})))) | ||
Theorem | pw2f1o 8065* | The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of [TakeutiZaring] p. 96. (Contributed by Mario Carneiro, 6-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑥, 𝐶, 𝐵))) ⇒ ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→({𝐵, 𝐶} ↑𝑚 𝐴)) | ||
Theorem | pw2eng 8066 | The power set of a set is equinumerous to set exponentiation with a base of ordinal 2𝑜. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 1-Jul-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≈ (2𝑜 ↑𝑚 𝐴)) | ||
Theorem | pw2en 8067 | The power set of a set is equinumerous to set exponentiation with a base of ordinal 2. Proposition 10.44 of [TakeutiZaring] p. 96. This is Metamath 100 proof #52. (Contributed by NM, 29-Jan-2004.) (Proof shortened by Mario Carneiro, 1-Jul-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝒫 𝐴 ≈ (2𝑜 ↑𝑚 𝐴) | ||
Theorem | fopwdom 8068 | Covering implies injection on power sets. (Contributed by Stefan O'Rear, 6-Nov-2014.) (Revised by Mario Carneiro, 24-Jun-2015.) (Revised by AV, 18-Sep-2021.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝒫 𝐵 ≼ 𝒫 𝐴) | ||
Theorem | enfixsn 8069* | Given two equipollent sets, a bijection can always be chosen which fixes a single point. (Contributed by Stefan O'Rear, 9-Jul-2015.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑋 ≈ 𝑌) → ∃𝑓(𝑓:𝑋–1-1-onto→𝑌 ∧ (𝑓‘𝐴) = 𝐵)) | ||
Theorem | sbthlem1 8070* | Lemma for sbth 8080. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) | ||
Theorem | sbthlem2 8071* | Lemma for sbth 8080. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷) | ||
Theorem | sbthlem3 8072* | Lemma for sbth 8080. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) | ||
Theorem | sbthlem4 8073* | Lemma for sbth 8080. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) | ||
Theorem | sbthlem5 8074* | Lemma for sbth 8080. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴) | ||
Theorem | sbthlem6 8075* | Lemma for sbth 8080. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((ran 𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) | ||
Theorem | sbthlem7 8076* | Lemma for sbth 8080. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) | ||
Theorem | sbthlem8 8077* | Lemma for sbth 8080. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun ◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) | ||
Theorem | sbthlem9 8078* | Lemma for sbth 8080. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | sbthlem10 8079* | Lemma for sbth 8080. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbth 8080 | Schroeder-Bernstein Theorem. Theorem 18 of [Suppes] p. 95. This theorem states that if set 𝐴 is smaller (has lower cardinality) than 𝐵 and vice-versa, then 𝐴 and 𝐵 are equinumerous (have the same cardinality). The interesting thing is that this can be proved without invoking the Axiom of Choice, as we do here, but the proof as you can see is quite difficult. (The theorem can be proved more easily if we allow AC.) The main proof consists of lemmas sbthlem1 8070 through sbthlem10 8079; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 8079. We follow closely the proof in Suppes, which you should consult to understand our proof at a higher level. Note that Suppes' proof, which is credited to J. M. Whitaker, does not require the Axiom of Infinity. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbthb 8081 | Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ 𝐴 ≈ 𝐵) | ||
Theorem | sbthcl 8082 | Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.) |
⊢ ≈ = ( ≼ ∩ ◡ ≼ ) | ||
Theorem | dfsdom2 8083 | Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.) |
⊢ ≺ = ( ≼ ∖ ◡ ≼ ) | ||
Theorem | brsdom2 8084 | Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴)) | ||
Theorem | sdomnsym 8085 | Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.) |
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴) | ||
Theorem | domnsym 8086 | Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) |
⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴) | ||
Theorem | 0domg 8087 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴) | ||
Theorem | dom0 8088 | A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) |
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅) | ||
Theorem | 0sdomg 8089 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) |
⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | 0dom 8090 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∅ ≼ 𝐴 | ||
Theorem | 0sdom 8091 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅) | ||
Theorem | sdom0 8092 | The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) |
⊢ ¬ 𝐴 ≺ ∅ | ||
Theorem | sdomdomtr 8093 | Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | sdomentr 8094 | Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.) |
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | domsdomtr 8095 | Transitivity of dominance and strict dominance. Theorem 22(ii) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | ensdomtr 8096 | Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | sdomirr 8097 | Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.) |
⊢ ¬ 𝐴 ≺ 𝐴 | ||
Theorem | sdomtr 8098 | Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.) |
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | sdomn2lp 8099 | Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.) |
⊢ ¬ (𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴) | ||
Theorem | enen1 8100 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |