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