P. 92 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9101-9200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xpcomen 9101	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 9102	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))
Theorem	xpsnen2g 9103	A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵)
Theorem	xpassen 9104	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 9105	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 9106	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Theorem	xpdom1g 9107	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 9108	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 9109	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 9110	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 9111*	Lemma for omxpen 9112. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦))    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵))
Theorem	omxpen 9112	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 9113*	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 9114*	Lemma for pw2f1o 9115. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑m 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶}))))
Theorem	pw2f1o 9115*	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 9116	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 9117	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 9118	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 9119*	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 9120	Obsolete version of sucdom2 9240 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 𝐴 ≼ 𝐵)
2.4.30  Schroeder-Bernstein Theorem
Theorem	sbthlem1 9121*	Lemma for sbth 9131. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))))
Theorem	sbthlem2 9122*	Lemma for sbth 9131. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷)
Theorem	sbthlem3 9123*	Lemma for sbth 9131. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷))
Theorem	sbthlem4 9124*	Lemma for sbth 9131. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷)))
Theorem	sbthlem5 9125*	Lemma for sbth 9131. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴)
Theorem	sbthlem6 9126*	Lemma for sbth 9131. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((ran 𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵)
Theorem	sbthlem7 9127*	Lemma for sbth 9131. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻)
Theorem	sbthlem8 9128*	Lemma for sbth 9131. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun ◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻)
Theorem	sbthlem9 9129*	Lemma for sbth 9131. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	sbthlem10 9130*	Lemma for sbth 9131. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbth 9131	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 9121 through sbthlem10 9130; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9130. 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 9130. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbthb 9132	Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ 𝐴 ≈ 𝐵)
Theorem	sbthcl 9133	Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = ( ≼ ∩ ◡ ≼ )
Theorem	dfsdom2 9134	Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
⊢ ≺ = ( ≼ ∖ ◡ ≼ )
Theorem	brsdom2 9135	Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴))
Theorem	sdomnsym 9136	Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴)
Theorem	domnsym 9137	Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴)
Theorem	0domg 9138	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5370, ax-un 7753. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
Theorem	0domgOLD 9139	Obsolete version of 0domg 9138 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
Theorem	dom0 9140	A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) Avoid ax-pow 5370, ax-un 7753. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅)
Theorem	dom0OLD 9141	Obsolete version of dom0 9140 as of 29-Nov-2024. (Contributed by NM, 22-Nov-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅)
Theorem	0sdomg 9142	A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5370, ax-un 7753. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	0sdomgOLD 9143	Obsolete version of 0sdomg 9142 as of 29-Nov-2024. (Contributed by NM, 23-Mar-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	0dom 9144	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∅ ≼ 𝐴
Theorem	0sdom 9145	A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)
Theorem	sdom0 9146	The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) Avoid ax-pow 5370, ax-un 7753. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ¬ 𝐴 ≺ ∅
Theorem	sdom0OLD 9147	Obsolete version of sdom0 9146 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ 𝐴 ≺ ∅
Theorem	sdomdomtr 9148	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 9149	Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.)
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	domsdomtr 9150	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 9151	Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sdomirr 9152	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.)
⊢ ¬ 𝐴 ≺ 𝐴
Theorem	sdomtr 9153	Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.)
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sdomn2lp 9154	Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.)
⊢ ¬ (𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴)
Theorem	enen1 9155	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶))
Theorem	enen2 9156	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵))
Theorem	domen1 9157	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶))
Theorem	domen2 9158	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵))
Theorem	sdomen1 9159	Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≺ 𝐶 ↔ 𝐵 ≺ 𝐶))
Theorem	sdomen2 9160	Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≺ 𝐴 ↔ 𝐶 ≺ 𝐵))
Theorem	domtriord 9161	Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	sdomel 9162	For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≺ 𝐵 → 𝐴 ∈ 𝐵))
Theorem	sdomdif 9163	The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.)
⊢ (𝐴 ≺ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	onsdominel 9164	An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐴 ∩ 𝐶) ≺ (𝐵 ∩ 𝐶)) → 𝐴 ∈ 𝐵)
Theorem	domunsn 9165	Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≺ 𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵)
Theorem	fodomr 9166*	There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.)
⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)
Theorem	pwdom 9167	Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵)
Theorem	canth2 9168	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 7384. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≺ 𝒫 𝐴
Theorem	canth2g 9169	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 9170	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 9171	No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴)
Theorem	disjen 9172	A stronger form of pwuninel 8298. We can use pwuninel 8298, 2pwuninel 9170 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 9173*	Existence version of disjen 9172. (Contributed by Mario Carneiro, 7-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥((𝐴 ∩ 𝑥) = ∅ ∧ 𝑥 ≈ 𝐵))
Theorem	domss2 9174	A corollary of disjenex 9173. 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 9175*	A corollary of disjenex 9173. 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 9176*	Weakening of domssex2 9175 to forget the functions in favor of dominance and equinumerosity. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 ≼ 𝐵 → ∃𝑥(𝐴 ⊆ 𝑥 ∧ 𝐵 ≈ 𝑥))
2.4.31  Equinumerosity (cont.)
Theorem	xpf1o 9177*	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 9178	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 9179	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 9180	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 9181	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 9182*	Lemma for xpmapen 9183. (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 9183	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 9184	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 9185	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 9186	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 9187	Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 ↑m 𝐵))
Theorem	pwen 9188	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 9189*	Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)})
Theorem	limenpsi 9190	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 9191	A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ Lim 𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴)
Theorem	limensuc 9192	A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ≈ suc 𝐴)
Theorem	infensuc 9193	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 𝐴)
2.4.32  Finite sets
Theorem	dif1enlem 9194	Lemma for rexdif1en 9196 and dif1en 9198. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7753. (Revised by BTernaryTau, 5-Jan-2025.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On) ∧ 𝐹:𝐴–1-1-onto→suc 𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀)
Theorem	dif1enlemOLD 9195	Obsolete version of dif1enlem 9194 as of 5-Jan-2025. (Contributed by BTernaryTau, 18-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑀 ∈ ω ∧ 𝐹:𝐴–1-1-onto→suc 𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀)
Theorem	rexdif1en 9196*	If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals and avoid ax-un 7753. (Revised by BTernaryTau, 5-Jan-2025.)
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀)
Theorem	rexdif1enOLD 9197*	Obsolete version of rexdif1en 9196 as of 5-Jan-2025. (Contributed by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀)
Theorem	dif1en 9198	If a set 𝐴 is equinumerous to the successor of an ordinal 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5370. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	dif1ennn 9199	If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9308. (Contributed by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	dif1enOLD 9200	Obsolete version of dif1en 9198 as of 6-Jan-2025. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Stefan O'Rear, 16-Aug-2015.) Avoid ax-pow 5370. (Revised by BTernaryTau, 26-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)