P. 91 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9001-9100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xp1en 9001	One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴)
Theorem	endisj 9002*	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 9003	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 5307. (Revised by BTernaryTau, 4-Dec-2024.)
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷))
Theorem	xpcomf1o 9004*	The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴)
Theorem	xpcomco 9005*	Composition with the bijection of xpcomf1o 9004 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    &   ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	xpcomen 9006	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 9007	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))
Theorem	xpsnen2g 9008	A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵)
Theorem	xpassen 9009	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 9010	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 9011	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Theorem	xpdom1g 9012	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 9013	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 9014	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 9015	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 9016*	Lemma for omxpen 9017. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦))    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵))
Theorem	omxpen 9017	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 9018*	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 9019*	Lemma for pw2f1o 9020. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑m 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶}))))
Theorem	pw2f1o 9020*	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 9021	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 9022	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 9023	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 9024*	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→𝑌 ∧ (𝑓‘𝐴) = 𝐵))
2.4.30  Schroeder-Bernstein Theorem
Theorem	sbthlem1 9025*	Lemma for sbth 9035. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))))
Theorem	sbthlem2 9026*	Lemma for sbth 9035. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷)
Theorem	sbthlem3 9027*	Lemma for sbth 9035. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷))
Theorem	sbthlem4 9028*	Lemma for sbth 9035. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷)))
Theorem	sbthlem5 9029*	Lemma for sbth 9035. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴)
Theorem	sbthlem6 9030*	Lemma for sbth 9035. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((ran 𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵)
Theorem	sbthlem7 9031*	Lemma for sbth 9035. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻)
Theorem	sbthlem8 9032*	Lemma for sbth 9035. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun ◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻)
Theorem	sbthlem9 9033*	Lemma for sbth 9035. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	sbthlem10 9034*	Lemma for sbth 9035. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbth 9035	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 9025 through sbthlem10 9034; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9034. 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 9034. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbthb 9036	Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ 𝐴 ≈ 𝐵)
Theorem	sbthcl 9037	Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = ( ≼ ∩ ◡ ≼ )
Theorem	dfsdom2 9038	Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
⊢ ≺ = ( ≼ ∖ ◡ ≼ )
Theorem	brsdom2 9039	Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴))
Theorem	sdomnsym 9040	Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴)
Theorem	domnsym 9041	Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴)
Theorem	0domg 9042	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-pow 5307, ax-un 7689. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ∈ 𝑉 → ∅ ≼ 𝐴)
Theorem	dom0 9043	A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004.) Avoid ax-pow 5307, ax-un 7689. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ≼ ∅ ↔ 𝐴 = ∅)
Theorem	0sdomg 9044	A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 23-Mar-2006.) Avoid ax-pow 5307, ax-un 7689. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ∈ 𝑉 → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅))
Theorem	0dom 9045	Any set dominates the empty set. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∅ ≼ 𝐴
Theorem	0sdom 9046	A set strictly dominates the empty set iff it is not empty. (Contributed by NM, 29-Jul-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)
Theorem	sdom0 9047	The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003.) Avoid ax-pow 5307, ax-un 7689. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ¬ 𝐴 ≺ ∅
Theorem	sdomdomtr 9048	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 9049	Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.)
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	domsdomtr 9050	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 9051	Transitivity of equinumerosity and strict dominance. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sdomirr 9052	Strict dominance is irreflexive. Theorem 21(i) of [Suppes] p. 97. (Contributed by NM, 4-Jun-1998.)
⊢ ¬ 𝐴 ≺ 𝐴
Theorem	sdomtr 9053	Strict dominance is transitive. Theorem 21(iii) of [Suppes] p. 97. (Contributed by NM, 9-Jun-1998.)
⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐶) → 𝐴 ≺ 𝐶)
Theorem	sdomn2lp 9054	Strict dominance has no 2-cycle loops. (Contributed by NM, 6-May-2008.)
⊢ ¬ (𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴)
Theorem	enen1 9055	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≈ 𝐶 ↔ 𝐵 ≈ 𝐶))
Theorem	enen2 9056	Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≈ 𝐴 ↔ 𝐶 ≈ 𝐵))
Theorem	domen1 9057	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐶 ↔ 𝐵 ≼ 𝐶))
Theorem	domen2 9058	Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≼ 𝐴 ↔ 𝐶 ≼ 𝐵))
Theorem	sdomen1 9059	Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ≺ 𝐶 ↔ 𝐵 ≺ 𝐶))
Theorem	sdomen2 9060	Equality-like theorem for equinumerosity and strict dominance. (Contributed by NM, 8-Nov-2003.)
⊢ (𝐴 ≈ 𝐵 → (𝐶 ≺ 𝐴 ↔ 𝐶 ≺ 𝐵))
Theorem	domtriord 9061	Dominance is trichotomous in the restricted case of ordinal numbers. (Contributed by Jeff Hankins, 24-Oct-2009.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	sdomel 9062	For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ≺ 𝐵 → 𝐴 ∈ 𝐵))
Theorem	sdomdif 9063	The difference of a set from a smaller set cannot be empty. (Contributed by Mario Carneiro, 5-Feb-2013.)
⊢ (𝐴 ≺ 𝐵 → (𝐵 ∖ 𝐴) ≠ ∅)
Theorem	onsdominel 9064	An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ (𝐴 ∩ 𝐶) ≺ (𝐵 ∩ 𝐶)) → 𝐴 ∈ 𝐵)
Theorem	domunsn 9065	Dominance over a set with one element added. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ (𝐴 ≺ 𝐵 → (𝐴 ∪ {𝐶}) ≼ 𝐵)
Theorem	fodomr 9066*	There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.)
⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)
Theorem	pwdom 9067	Injection of sets implies injection on power sets. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐴 ≼ 𝐵 → 𝒫 𝐴 ≼ 𝒫 𝐵)
Theorem	canth2 9068	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 7321. This is Metamath 100 proof #63. (Contributed by NM, 7-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≺ 𝒫 𝐴
Theorem	canth2g 9069	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 9070	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 9071	No set equals the power set of its power set. (Contributed by NM, 17-Nov-2008.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝒫 𝐴 ≠ 𝐴)
Theorem	disjen 9072	A stronger form of pwuninel 8225. We can use pwuninel 8225, 2pwuninel 9070 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 9073*	Existence version of disjen 9072. (Contributed by Mario Carneiro, 7-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∃𝑥((𝐴 ∩ 𝑥) = ∅ ∧ 𝑥 ≈ 𝐵))
Theorem	domss2 9074	A corollary of disjenex 9073. 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 9075*	A corollary of disjenex 9073. 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 9076*	Weakening of domssex2 9075 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 9077*	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 9078	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 9079	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 9080	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 9081	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 9082*	Lemma for xpmapen 9083. (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 9083	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 9084	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 9085	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 9086	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 9087	Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 17-Jul-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐴 ≼ (𝐴 ↑m 𝐵))
Theorem	pwen 9088	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 9089*	Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶)} ≈ {𝑥 ∣ (𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶)})
Theorem	limenpsi 9090	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 9091	A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ Lim 𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ suc 𝐴)
Theorem	limensuc 9092	A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003.)
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → 𝐴 ≈ suc 𝐴)
Theorem	infensuc 9093	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 9094	Lemma for rexdif1en 9095 and dif1en 9096. (Contributed by BTernaryTau, 18-Aug-2024.) Generalize to all ordinals and add a sethood requirement to avoid ax-un 7689. (Revised by BTernaryTau, 5-Jan-2025.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝑀 ∈ On) ∧ 𝐹:𝐴–1-1-onto→suc 𝑀) → (𝐴 ∖ {(◡𝐹‘𝑀)}) ≈ 𝑀)
Theorem	rexdif1en 9095*	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 7689. (Revised by BTernaryTau, 5-Jan-2025.)
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ 𝐴 (𝐴 ∖ {𝑥}) ≈ 𝑀)
Theorem	dif1en 9096	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 5307. (Revised by BTernaryTau, 26-Aug-2024.) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	dif1ennn 9097	If a set 𝐴 is equinumerous to the successor of a natural number 𝑀, then 𝐴 with an element removed is equinumerous to 𝑀. See also dif1ennnALT 9187. (Contributed by BTernaryTau, 6-Jan-2025.)
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀)
Theorem	findcard 9098*	Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = (𝑦 ∖ {𝑧}) → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ Fin → (∀𝑧 ∈ 𝑦 𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard2 9099*	Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.) Avoid ax-pow 5307. (Revised by BTernaryTau, 26-Aug-2024.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ Fin → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)
Theorem	findcard2s 9100*	Variation of findcard2 9099 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ Fin → 𝜏)