![]() |
Metamath
Proof Explorer Theorem List (p. 91 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ensym 9001 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | ||
Theorem | ensymi 9002 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 | ||
Theorem | ensymd 9003 | Symmetry of equinumerosity. Deduction form of ensym 9001. (Contributed by David Moews, 1-May-2017.) |
⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) | ||
Theorem | entr 9004 | Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
Theorem | domtr 9005 | 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 9006 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 | ||
Theorem | entr2i 9007 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 | ||
Theorem | entr3i 9008 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 | ||
Theorem | entr4i 9009 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 | ||
Theorem | endomtr 9010 | Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | domentr 9011 | Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) | ||
Theorem | f1imaeng 9012 | If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | f1imaen2g 9013 | If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (This version of f1imaeng 9012 does not need ax-rep 5284.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | f1imaen 9014 | If a function is one-to-one, then the image of a subset of its domain under it is equinumerous to the subset. (Contributed by NM, 30-Sep-2004.) |
⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
Theorem | en0 9015 | The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5362, ax-un 7727. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | ||
Theorem | en0OLD 9016 | Obsolete version of en0 9015 as of 23-Sep-2024. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5362. (Revised by BTernaryTau, 31-Jul-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | ||
Theorem | en0ALT 9017 | Shorter proof of en0 9015, depending on ax-pow 5362 and ax-un 7727. (Contributed by NM, 27-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | ||
Theorem | en0r 9018 | The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024.) |
⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅) | ||
Theorem | ensn1 9019 | A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7727. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o | ||
Theorem | ensn1OLD 9020 | Obsolete version of ensn1 9019 as of 23-Sep-2024. (Contributed by NM, 4-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o | ||
Theorem | ensn1g 9021 | A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o) | ||
Theorem | enpr1g 9022 | {𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.) |
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o) | ||
Theorem | en1 9023* | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.) Avoid ax-un 7727. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | en1OLD 9024* | Obsolete version of en1 9023 as of 23-Sep-2024. (Contributed by NM, 25-Jul-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | en1b 9025 | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) Avoid ax-un 7727. (Revised by BTernaryTau, 24-Sep-2024.) |
⊢ (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴}) | ||
Theorem | en1bOLD 9026 | Obsolete version of en1b 9025 as of 24-Sep-2024. (Contributed by Mario Carneiro, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴}) | ||
Theorem | reuen1 9027* | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o) | ||
Theorem | euen1 9028 | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o) | ||
Theorem | euen1b 9029* | Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴) | ||
Theorem | en1uniel 9030 | A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.) Avoid ax-un 7727. (Revised by BTernaryTau, 24-Sep-2024.) |
⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | en1unielOLD 9031 | Obsolete version of en1uniel 9030 as of 24-Sep-2024. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆) | ||
Theorem | 2dom 9032* | A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.) |
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) | ||
Theorem | fundmen 9033 | 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 9034 | A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.) |
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) | ||
Theorem | cnven 9035 | A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) | ||
Theorem | cnvct 9036 | If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) | ||
Theorem | fndmeng 9037 | A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) | ||
Theorem | mapsnend 9038 | 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.) (Revised by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ↑m {𝐵}) ≈ 𝐴) | ||
Theorem | mapsnen 9039 | 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.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m {𝐵}) ≈ 𝐴 | ||
Theorem | snmapen 9040 | Set exponentiation: a singleton to any set is equinumerous to that singleton. (Contributed by NM, 17-Dec-2003.) (Revised by AV, 17-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} ↑m 𝐵) ≈ {𝐴}) | ||
Theorem | snmapen1 9041 | Set exponentiation: a singleton to any set is equinumerous to ordinal 1. (Proposed by BJ, 17-Jul-2022.) (Contributed by AV, 17-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} ↑m 𝐵) ≈ 1o) | ||
Theorem | map1 9042 | 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.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (1o ↑m 𝐴) ≈ 1o) | ||
Theorem | en2sn 9043 | Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5362. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7727. (Revised by BTernaryTau, 25-Sep-2024.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) | ||
Theorem | en2snOLD 9044 | Obsolete version of en2sn 9043 as of 25-Sep-2024. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5362. (Revised by BTernaryTau, 31-Jul-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) | ||
Theorem | en2snOLDOLD 9045 | Obsolete version of en2sn 9043 as of 31-Jul-2024. (Contributed by NM, 9-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) | ||
Theorem | snfi 9046 | A singleton is finite. (Contributed by NM, 4-Nov-2002.) |
⊢ {𝐴} ∈ Fin | ||
Theorem | fiprc 9047 | The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.) |
⊢ Fin ∉ V | ||
Theorem | unen 9048 | 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 | enrefnn 9049 | Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg 8982). (Contributed by BTernaryTau, 31-Jul-2024.) |
⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴) | ||
Theorem | en2prd 9050 | Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷}) | ||
Theorem | enpr2d 9051 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-un 7727. (Revised by BTernaryTau, 23-Dec-2024.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | enpr2dOLD 9052 | Obsolete version of enpr2d 9051 as of 23-Dec-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | ssct 9053 | Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5362, ax-un 7727. (Revised by BTernaryTau, 7-Dec-2024.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) | ||
Theorem | ssctOLD 9054 | Obsolete version of ssct 9053 as of 7-Dec-2024. (Contributed by Thierry Arnoux, 31-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) | ||
Theorem | difsnen 9055 | All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})) | ||
Theorem | domdifsn 9056 | 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 9057 | 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 9058 | 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 9059 | One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴) | ||
Theorem | endisj 9060* | Any two sets are equinumerous to two disjoint sets. Exercise 4.39 of [Mendelson] p. 255. (Contributed by NM, 16-Apr-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∃𝑥∃𝑦((𝑥 ≈ 𝐴 ∧ 𝑦 ≈ 𝐵) ∧ (𝑥 ∩ 𝑦) = ∅) | ||
Theorem | undom 9061 | 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.) Avoid ax-pow 5362. (Revised by BTernaryTau, 4-Dec-2024.) |
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) | ||
Theorem | undomOLD 9062 | Obsolete version of undom 9061 as of 4-Dec-2024. (Contributed by NM, 3-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) | ||
Theorem | xpcomf1o 9063* | The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) | ||
Theorem | xpcomco 9064* | Composition with the bijection of xpcomf1o 9063 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) & ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | xpcomen 9065 | 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 9066 | Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) | ||
Theorem | xpsnen2g 9067 | A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵) | ||
Theorem | xpassen 9068 | 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 9069 | 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 9070 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) | ||
Theorem | xpdom1g 9071 | 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 9072 | 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 9073 | 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 9074 | 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 9075* | Lemma for omxpen 9076. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵)) | ||
Theorem | omxpen 9076 | The cardinal and ordinal products are always equinumerous. Exercise 10 of [TakeutiZaring] p. 89. (Contributed by Mario Carneiro, 3-Mar-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ≈ (𝐴 × 𝐵)) | ||
Theorem | omf1o 9077* | Construct an explicit bijection from 𝐴 ·o 𝐵 to 𝐵 ·o 𝐴. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦)) & ⊢ 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐵 ·o 𝑦) +o 𝑥)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐺 ∘ ◡𝐹):(𝐴 ·o 𝐵)–1-1-onto→(𝐵 ·o 𝐴)) | ||
Theorem | pw2f1olem 9078* | Lemma for pw2f1o 9079. (Contributed by Mario Carneiro, 6-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑m 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶})))) | ||
Theorem | pw2f1o 9079* | 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→({𝐵, 𝐶} ↑m 𝐴)) | ||
Theorem | pw2eng 9080 | The power set of a set is equinumerous to set exponentiation with a base of ordinal 2o. (Contributed by FL, 22-Feb-2011.) (Revised by Mario Carneiro, 1-Jul-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ≈ (2o ↑m 𝐴)) | ||
Theorem | pw2en 9081 | 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 ⇒ ⊢ 𝒫 𝐴 ≈ (2o ↑m 𝐴) | ||
Theorem | fopwdom 9082 | 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 9083* | 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 | sucdom2OLD 9084 | Obsolete version of sucdom2 9208 as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≺ 𝐵 → suc 𝐴 ≼ 𝐵) | ||
Theorem | sbthlem1 9085* | Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) | ||
Theorem | sbthlem2 9086* | Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷) | ||
Theorem | sbthlem3 9087* | Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) | ||
Theorem | sbthlem4 9088* | Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) | ||
Theorem | sbthlem5 9089* | Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴) | ||
Theorem | sbthlem6 9090* | Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((ran 𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) | ||
Theorem | sbthlem7 9091* | Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) | ||
Theorem | sbthlem8 9092* | Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun ◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) | ||
Theorem | sbthlem9 9093* | Lemma for sbth 9095. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | sbthlem10 9094* | Lemma for sbth 9095. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbth 9095 |
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. The theorem can
also be proved from the axiom of choice and the linear order of the
cardinal numbers, but our development does not provide the linear order
of cardinal numbers until much later and in ways that depend on
Schroeder-Bernstein.
The main proof consists of lemmas sbthlem1 9085 through sbthlem10 9094; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9094. 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. In the Intuitionistic Logic Explorer (ILE) the Schroeder-Bernstein Theorem has been proven equivalent to the law of the excluded middle (LEM), and in ILE the LEM is not accepted as necessarily true; see https://us.metamath.org/ileuni/exmidsbth.html 9094. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbthb 9096 | Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ 𝐴 ≈ 𝐵) | ||
Theorem | sbthcl 9097 | Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.) |
⊢ ≈ = ( ≼ ∩ ◡ ≼ ) | ||
Theorem | dfsdom2 9098 | Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.) |
⊢ ≺ = ( ≼ ∖ ◡ ≼ ) | ||
Theorem | brsdom2 9099 | Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴)) | ||
Theorem | sdomnsym 9100 | Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.) |
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |