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