| Metamath
Proof Explorer Theorem List (p. 91 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | brdom 9001* | Dominance relation. (Contributed by NM, 15-Jun-1998.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) | ||
| Theorem | domen 9002* | Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) | ||
| Theorem | domeng 9003* | 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 9004 | A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.) |
| ⊢ (𝐴 ≼ ω → 𝐴 ∈ V) | ||
| Theorem | f1oen4g 9005 | The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 9011 does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| ⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
| Theorem | f1dom4g 9006 | The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 9012 does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| ⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
| Theorem | f1oen3g 9007 | The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 9011 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
| Theorem | f1dom3g 9008 | The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 9012 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by BTernaryTau, 9-Sep-2024.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
| Theorem | f1oen2g 9009 | The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 9011 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
| Theorem | f1dom2g 9010 | The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 9012 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) (Proof shortened by BTernaryTau, 25-Sep-2024.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵) | ||
| Theorem | f1oeng 9011 | The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | ||
| Theorem | f1domg 9012 | The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.) |
| ⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)) | ||
| Theorem | f1oen 9013 | 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 9014 | The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵) | ||
| Theorem | brsdom 9015 | Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.) |
| ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵)) | ||
| Theorem | isfi 9016* | 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 9017 | Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.) |
| ⊢ ≈ ⊆ ≼ | ||
| Theorem | dfdom2 9018 | Alternate definition of dominance. (Contributed by NM, 17-Jun-1998.) |
| ⊢ ≼ = ( ≺ ∪ ≈ ) | ||
| Theorem | endom 9019 | Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.) |
| ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵) | ||
| Theorem | sdomdom 9020 | Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.) |
| ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) | ||
| Theorem | sdomnen 9021 | Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.) |
| ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵) | ||
| Theorem | brdom2 9022 | Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.) |
| ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵)) | ||
| Theorem | bren2 9023 | Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.) |
| ⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵)) | ||
| Theorem | enrefg 9024 | Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) | ||
| Theorem | enref 9025 | Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≈ 𝐴 | ||
| Theorem | eqeng 9026 | Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) | ||
| Theorem | domrefg 9027 | Dominance is reflexive. (Contributed by NM, 18-Jun-1998.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴) | ||
| Theorem | en2d 9028* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝑋)) & ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝑌)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
| Theorem | en3d 9029* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)) & ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))) ⇒ ⊢ (𝜑 → 𝐴 ≈ 𝐵) | ||
| Theorem | en2i 9030* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷)) ⇒ ⊢ 𝐴 ≈ 𝐵 | ||
| Theorem | en3i 9031* | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵) & ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶)) ⇒ ⊢ 𝐴 ≈ 𝐵 | ||
| Theorem | dom2lem 9032* | 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 9033* | 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 9034* | 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 9035* | 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 9036* | 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 9037 | Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) |
| ⊢ I ⊆ ≈ | ||
| Theorem | domssl 9038 | If 𝐴 is a subset of 𝐵 and 𝐶 dominates 𝐵, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
| Theorem | domssr 9039 | If 𝐶 is a superset of 𝐵 and 𝐵 dominates 𝐴, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.) |
| ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐶) | ||
| Theorem | ssdomg 9040 | 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 9041 | 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 | ensymb 9042 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.) |
| ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴) | ||
| Theorem | ensym 9043 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
| ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | ||
| Theorem | ensymi 9044 | Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
| ⊢ 𝐴 ≈ 𝐵 ⇒ ⊢ 𝐵 ≈ 𝐴 | ||
| Theorem | ensymd 9045 | Symmetry of equinumerosity. Deduction form of ensym 9043. (Contributed by David Moews, 1-May-2017.) |
| ⊢ (𝜑 → 𝐴 ≈ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≈ 𝐴) | ||
| Theorem | entr 9046 | Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶) | ||
| Theorem | domtr 9047 | 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 9048 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
| ⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐴 ≈ 𝐶 | ||
| Theorem | entr2i 9049 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
| ⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐵 ≈ 𝐶 ⇒ ⊢ 𝐶 ≈ 𝐴 | ||
| Theorem | entr3i 9050 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
| ⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐴 ≈ 𝐶 ⇒ ⊢ 𝐵 ≈ 𝐶 | ||
| Theorem | entr4i 9051 | A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.) |
| ⊢ 𝐴 ≈ 𝐵 & ⊢ 𝐶 ≈ 𝐵 ⇒ ⊢ 𝐴 ≈ 𝐶 | ||
| Theorem | endomtr 9052 | Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.) |
| ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | ||
| Theorem | domentr 9053 | Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.) |
| ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶) | ||
| Theorem | f1imaeng 9054 | 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 9055 | 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 9054 does not need ax-rep 5279.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.) |
| ⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶) | ||
| Theorem | f1imaen3g 9056 | If a set function is one-to-one, then a subset of its domain is equinumerous to the image of that subset. (This version of f1imaeng 9054 does not need ax-rep 5279 nor ax-pow 5365.) (Contributed by BTernaryTau, 13-Jan-2025.) |
| ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉) → 𝐶 ≈ (𝐹 “ 𝐶)) | ||
| Theorem | f1imaen 9057 | 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 9058 | The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | ||
| Theorem | en0ALT 9059 | Shorter proof of en0 9058, depending on ax-pow 5365 and ax-un 7755. (Contributed by NM, 27-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅) | ||
| Theorem | en0r 9060 | The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024.) |
| ⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅) | ||
| Theorem | ensn1 9061 | A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002.) Avoid ax-un 7755. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ {𝐴} ≈ 1o | ||
| Theorem | ensn1g 9062 | A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o) | ||
| Theorem | enpr1g 9063 | {𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.) |
| ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o) | ||
| Theorem | en1 9064* | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004.) Avoid ax-un 7755. (Revised by BTernaryTau, 23-Sep-2024.) |
| ⊢ (𝐴 ≈ 1o ↔ ∃𝑥 𝐴 = {𝑥}) | ||
| Theorem | en1b 9065 | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) Avoid ax-un 7755. (Revised by BTernaryTau, 24-Sep-2024.) |
| ⊢ (𝐴 ≈ 1o ↔ 𝐴 = {∪ 𝐴}) | ||
| Theorem | reuen1 9066* | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
| ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o) | ||
| Theorem | euen1 9067 | Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.) |
| ⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o) | ||
| Theorem | euen1b 9068* | Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.) |
| ⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴) | ||
| Theorem | en1uniel 9069 | A singleton contains its sole element. (Contributed by Stefan O'Rear, 16-Aug-2015.) Avoid ax-un 7755. (Revised by BTernaryTau, 24-Sep-2024.) |
| ⊢ (𝑆 ≈ 1o → ∪ 𝑆 ∈ 𝑆) | ||
| Theorem | 2dom 9070* | A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.) |
| ⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦) | ||
| Theorem | fundmen 9071 | 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 9072 | A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.) |
| ⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹) | ||
| Theorem | cnven 9073 | A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.) |
| ⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴) | ||
| Theorem | cnvct 9074 | If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.) |
| ⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω) | ||
| Theorem | fndmeng 9075 | A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹) | ||
| Theorem | mapsnend 9076 | 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 9077 | 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 9078 | 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 9079 | 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 9080 | 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 9081 | Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5365. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7755. (Revised by BTernaryTau, 25-Sep-2024.) |
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵}) | ||
| Theorem | 0fi 9082 | The empty set is finite. (Contributed by FL, 14-Jul-2008.) Avoid ax-10 2141, ax-un 7755. (Revised by BTernaryTau, 13-Jan-2025.) |
| ⊢ ∅ ∈ Fin | ||
| Theorem | snfi 9083 | A singleton is finite. (Contributed by NM, 4-Nov-2002.) (Proof shortened by BTernaryTau, 13-Jan-2025.) |
| ⊢ {𝐴} ∈ Fin | ||
| Theorem | snfiOLD 9084 | Obsolete version of snfi 9083 as of 13-Jan-2025. (Contributed by NM, 4-Nov-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ {𝐴} ∈ Fin | ||
| Theorem | fiprc 9085 | The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.) |
| ⊢ Fin ∉ V | ||
| Theorem | unen 9086 | 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 9087 | Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg 9024). (Contributed by BTernaryTau, 31-Jul-2024.) |
| ⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴) | ||
| Theorem | en2prd 9088 | Two unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷}) | ||
| Theorem | enpr2d 9089 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) Avoid ax-un 7755. (Revised by BTernaryTau, 23-Dec-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
| Theorem | enpr2dOLD 9090 | Obsolete version of enpr2d 9089 as of 23-Dec-2024. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐶) & ⊢ (𝜑 → 𝐵 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → {𝐴, 𝐵} ≈ 2o) | ||
| Theorem | ssct 9091 | Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5365, ax-un 7755. (Revised by BTernaryTau, 7-Dec-2024.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) | ||
| Theorem | ssctOLD 9092 | Obsolete version of ssct 9091 as of 7-Dec-2024. (Contributed by Thierry Arnoux, 31-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω) | ||
| Theorem | difsnen 9093 | All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵})) | ||
| Theorem | domdifsn 9094 | 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 9095 | 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 9096 | 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 9097 | One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴) | ||
| Theorem | endisj 9098* | 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 9099 | 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 5365. (Revised by BTernaryTau, 4-Dec-2024.) |
| ⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) | ||
| Theorem | undomOLD 9100 | Obsolete version of undom 9099 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.) |
| ⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |