Home | Metamath
Proof Explorer Theorem List (p. 87 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xpsnen 8601 | 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 8602 | 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 8603 | One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴) | ||
Theorem | endisj 8604* | 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 8605 | 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 8606* | The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) ⇒ ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) | ||
Theorem | xpcomco 8607* | Composition with the bijection of xpcomf1o 8606 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) & ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | ||
Theorem | xpcomen 8608 | 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 8609 | Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴)) | ||
Theorem | xpsnen2g 8610 | A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵) | ||
Theorem | xpassen 8611 | 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 8612 | 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 8613 | Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) | ||
Theorem | xpdom1g 8614 | 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 8615 | 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 8616 | 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 8617 | 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 8618* | Lemma for omxpen 8619. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦)) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵)) | ||
Theorem | omxpen 8619 | 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 8620* | 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 8621* | Lemma for pw2f1o 8622. (Contributed by Mario Carneiro, 6-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑m 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶})))) | ||
Theorem | pw2f1o 8622* | 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 8623 | 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 8624 | 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 8625 | 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 8626* | 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 8627* | Lemma for sbth 8637. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) | ||
Theorem | sbthlem2 8628* | Lemma for sbth 8637. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷) | ||
Theorem | sbthlem3 8629* | Lemma for sbth 8637. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (ran 𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) | ||
Theorem | sbthlem4 8630* | Lemma for sbth 8637. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} ⇒ ⊢ (((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) | ||
Theorem | sbthlem5 8631* | Lemma for sbth 8637. (Contributed by NM, 22-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴) | ||
Theorem | sbthlem6 8632* | Lemma for sbth 8637. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((ran 𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵) | ||
Theorem | sbthlem7 8633* | Lemma for sbth 8637. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) | ||
Theorem | sbthlem8 8634* | Lemma for sbth 8637. (Contributed by NM, 27-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((Fun ◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) | ||
Theorem | sbthlem9 8635* | Lemma for sbth 8637. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⇒ ⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) | ||
Theorem | sbthlem10 8636* | Lemma for sbth 8637. (Contributed by NM, 28-Mar-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} & ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbth 8637 |
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 8627 through sbthlem10 8636; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 8636. 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 8636. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) | ||
Theorem | sbthb 8638 | Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.) |
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ 𝐴 ≈ 𝐵) | ||
Theorem | sbthcl 8639 | Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.) |
⊢ ≈ = ( ≼ ∩ ◡ ≼ ) | ||
Theorem | dfsdom2 8640 | Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.) |
⊢ ≺ = ( ≼ ∖ ◡ ≼ ) | ||
Theorem | brsdom2 8641 | Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴)) | ||
Theorem | sdomnsym 8642 | Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.) |
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴) | ||
Theorem | domnsym 8643 | Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.) |
⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴) | ||
Theorem | 0domg 8644 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴) | ||
Theorem | dom0 8645 | A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) |
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅) | ||
Theorem | 0sdomg 8646 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) |
⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) | ||
Theorem | 0dom 8647 | Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ∅ ≼ 𝐴 | ||
Theorem | 0sdom 8648 | A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅) | ||
Theorem | sdom0 8649 | The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) |
⊢ ¬ 𝐴 ≺ ∅ | ||
Theorem | sdomdomtr 8650 | 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 8651 | Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.) |
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | domsdomtr 8652 | 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 8653 | Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | sdomirr 8654 | Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.) |
⊢ ¬ 𝐴 ≺ 𝐴 | ||
Theorem | sdomtr 8655 | Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.) |
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶) | ||
Theorem | sdomn2lp 8656 | Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.) |
⊢ ¬ (𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴) | ||
Theorem | enen1 8657 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶)) | ||
Theorem | enen2 8658 | Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵)) | ||
Theorem | domen1 8659 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶)) | ||
Theorem | domen2 8660 | Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵)) | ||
Theorem | sdomen1 8661 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≺ 𝐶 ↔ 𝐵 ≺ 𝐶)) | ||
Theorem | sdomen2 8662 | Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.) |
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≺ 𝐴 ↔ 𝐶 ≺ 𝐵)) | ||
Theorem | domtriord 8663 | Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | sdomel 8664 | Strict dominance implies ordinal membership. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≺ 𝐵 → 𝐴 ∈ 𝐵)) | ||
Theorem | sdomdif 8665 | The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.) |
⊢ (𝐴 ≺ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅) | ||
Theorem | onsdominel 8666 | An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐴 ∩ 𝐶) ≺ (𝐵 ∩ 𝐶)) → 𝐴 ∈ 𝐵) | ||
Theorem | domunsn 8667 | Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝐴 ≺ 𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵) | ||
Theorem | fodomr 8668* | There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.) |
⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵) | ||
Theorem | pwdom 8669 | Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵) | ||
Theorem | canth2 8670 | Cantor's Theorem. No set is equinumerous to its power set. Specifically, any set has a cardinality (size) strictly less than the cardinality of its power set. For example, the cardinality of real numbers is the same as the cardinality of the power set of integers, so real numbers cannot be put into a one-to-one correspondence with integers. Theorem 23 of [Suppes] p. 97. For the function version, see canth 7111. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ 𝐴 ≺ 𝒫 𝐴 | ||
Theorem | canth2g 8671 | Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97. (Contributed by NM, 7-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝒫 𝐴) | ||
Theorem | 2pwuninel 8672 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by NM, 27-Jun-2008.) |
⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 | ||
Theorem | 2pwne 8673 | No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.) |
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴) | ||
Theorem | disjen 8674 | A stronger form of pwuninel 7941. We can use pwuninel 7941, 2pwuninel 8672 to create one or two sets disjoint from a given set 𝐴, but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set 𝐵 we can construct a set 𝑥 that is equinumerous to it and disjoint from 𝐴. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∩ (𝐵 × {𝒫 ∪ ran 𝐴})) = ∅ ∧ (𝐵 × {𝒫 ∪ ran 𝐴}) ≈ 𝐵)) | ||
Theorem | disjenex 8675* | Existence version of disjen 8674. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥((𝐴 ∩ 𝑥) = ∅ ∧ 𝑥 ≈ 𝐵)) | ||
Theorem | domss2 8676 | A corollary of disjenex 8675. If 𝐹 is an injection from 𝐴 to 𝐵 then 𝐺 is a right inverse of 𝐹 from 𝐵 to a superset of 𝐴. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐺 = ◡(𝐹 ∪ (1st ↾ ((𝐵 ∖ ran 𝐹) × {𝒫 ∪ ran 𝐴}))) ⇒ ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐺:𝐵–1-1-onto→ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ (𝐺 ∘ 𝐹) = ( I ↾ 𝐴))) | ||
Theorem | domssex2 8677* | A corollary of disjenex 8675. If 𝐹 is an injection from 𝐴 to 𝐵 then there is a right inverse 𝑔 of 𝐹 from 𝐵 to a superset of 𝐴. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑔(𝑔:𝐵–1-1→V ∧ (𝑔 ∘ 𝐹) = ( I ↾ 𝐴))) | ||
Theorem | domssex 8678* | Weakening of domssex 8678 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥)) | ||
Theorem | xpf1o 8679* | Construct a bijection on a Cartesian product given bijections on the factors. (Contributed by Mario Carneiro, 30-May-2015.) |
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑋):𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑌):𝐶–1-1-onto→𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 〈𝑋, 𝑌〉):(𝐴 × 𝐶)–1-1-onto→(𝐵 × 𝐷)) | ||
Theorem | xpen 8680 | Equinumerosity law for Cartesian product. Proposition 4.22(b) of [Mendelson] p. 254. (Contributed by NM, 24-Jul-2004.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 × 𝐶) ≈ (𝐵 × 𝐷)) | ||
Theorem | mapen 8681 | Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of [Enderton] p. 139. (Contributed by NM, 16-Dec-2003.) (Proof shortened by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ↑m 𝐶) ≈ (𝐵 ↑m 𝐷)) | ||
Theorem | mapdom1 8682 | Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.) |
⊢ (𝐴 ≼ 𝐵 → (𝐴 ↑m 𝐶) ≼ (𝐵 ↑m 𝐶)) | ||
Theorem | mapxpen 8683 | Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96. (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ↑m 𝐵) ↑m 𝐶) ≈ (𝐴 ↑m (𝐵 × 𝐶))) | ||
Theorem | xpmapenlem 8684* | Lemma for xpmapen 8685. (Contributed by NM, 1-May-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V & ⊢ 𝐷 = (𝑧 ∈ 𝐶 ↦ (1st ‘(𝑥‘𝑧))) & ⊢ 𝑅 = (𝑧 ∈ 𝐶 ↦ (2nd ‘(𝑥‘𝑧))) & ⊢ 𝑆 = (𝑧 ∈ 𝐶 ↦ 〈((1st ‘𝑦)‘𝑧), ((2nd ‘𝑦)‘𝑧)〉) ⇒ ⊢ ((𝐴 × 𝐵) ↑m 𝐶) ≈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) | ||
Theorem | xpmapen 8685 | Equinumerosity law for set exponentiation of a Cartesian product. Exercise 4.47 of [Mendelson] p. 255. (Contributed by NM, 23-Feb-2004.) (Proof shortened by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((𝐴 × 𝐵) ↑m 𝐶) ≈ ((𝐴 ↑m 𝐶) × (𝐵 ↑m 𝐶)) | ||
Theorem | mapunen 8686 | Equinumerosity law for set exponentiation of a disjoint union. Exercise 4.45 of [Mendelson] p. 255. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐶 ↑m (𝐴 ∪ 𝐵)) ≈ ((𝐶 ↑m 𝐴) × (𝐶 ↑m 𝐵))) | ||
Theorem | map2xp 8687 | A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑m 2o) ≈ (𝐴 × 𝐴)) | ||
Theorem | mapdom2 8688 | Order-preserving property of set exponentiation. Theorem 6L(d) of [Enderton] p. 149. (Contributed by NM, 23-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ≼ 𝐵 ∧ ¬ (𝐴 = ∅ ∧ 𝐶 = ∅)) → (𝐶 ↑m 𝐴) ≼ (𝐶 ↑m 𝐵)) | ||
Theorem | mapdom3 8689 | Set exponentiation dominates the mantissa. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 ↑m 𝐵)) | ||
Theorem | pwen 8690 | If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of [TakeutiZaring] p. 87. (Contributed by NM, 29-Jan-2004.) (Revised by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵) | ||
Theorem | ssenen 8691* | Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)}) | ||
Theorem | limenpsi 8692 | A limit ordinal is equinumerous to a proper subset of itself. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ Lim 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ (𝐴 ∖ {∅})) | ||
Theorem | limensuci 8693 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ Lim 𝐴 ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴) | ||
Theorem | limensuc 8694 | A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.) |
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ≈ suc 𝐴) | ||
Theorem | infensuc 8695 | Any infinite ordinal is equinumerous to its successor. Exercise 7 of [TakeutiZaring] p. 88. Proved without the Axiom of Infinity. (Contributed by NM, 30-Oct-2003.) (Revised by Mario Carneiro, 13-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → 𝐴 ≈ suc 𝐴) | ||
Theorem | phplem1 8696 | Lemma for Pigeonhole Principle. If we join a natural number to itself minus an element, we end up with its successor minus the same element. (Contributed by NM, 25-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem2 8697 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus one of its elements. (Contributed by NM, 11-Jun-1998.) (Revised by Mario Carneiro, 16-Nov-2014.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem3 8698 | Lemma for Pigeonhole Principle. A natural number is equinumerous to its successor minus any element of the successor. (Contributed by NM, 26-May-1998.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ suc 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) | ||
Theorem | phplem4 8699 | Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers. (Contributed by NM, 28-May-1998.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ≈ suc 𝐵 → 𝐴 ≈ 𝐵)) | ||
Theorem | nneneq 8700 | Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136. (Contributed by NM, 28-May-1998.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |