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	dom2 9001*	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 9002*	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 9003	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ I ⊆ ≈
Theorem	domssl 9004	If 𝐴 is a subset of 𝐵 and 𝐶 dominates 𝐵, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domssr 9005	If 𝐶 is a superset of 𝐵 and 𝐵 dominates 𝐴, then 𝐶 also dominates 𝐴. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵) → 𝐴 ≼ 𝐶)
Theorem	ssdomg 9006	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 9007	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 9008	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
Theorem	ensym 9009	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
Theorem	ensymi 9010	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    ⇒   ⊢ 𝐵 ≈ 𝐴
Theorem	ensymd 9011	Symmetry of equinumerosity. Deduction form of ensym 9009. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≈ 𝐴)
Theorem	entr 9012	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92. (Contributed by NM, 9-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≈ 𝐶)
Theorem	domtr 9013	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 9014	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	entr2i 9015	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐵 ≈ 𝐶    ⇒   ⊢ 𝐶 ≈ 𝐴
Theorem	entr3i 9016	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐴 ≈ 𝐶    ⇒   ⊢ 𝐵 ≈ 𝐶
Theorem	entr4i 9017	A chained equinumerosity inference. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    &   ⊢ 𝐶 ≈ 𝐵    ⇒   ⊢ 𝐴 ≈ 𝐶
Theorem	endomtr 9018	Transitivity of equinumerosity and dominance. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	domentr 9019	Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≼ 𝐶)
Theorem	f1imaeng 9020	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 9021	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 9020 does not need ax-rep 5243.) (Contributed by Mario Carneiro, 16-Nov-2014.) (Revised by Mario Carneiro, 25-Jun-2015.)
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐶 ∈ 𝑉)) → (𝐹 “ 𝐶) ≈ 𝐶)
Theorem	f1imaen3g 9022	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 9020 does not need ax-rep 5243 nor ax-pow 5341.) (Contributed by BTernaryTau, 13-Jan-2025.)
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐹 ∈ 𝑉) → 𝐶 ≈ (𝐹 “ 𝐶))
Theorem	f1imaen 9023	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 9024	The empty set is equinumerous only to itself. Exercise 1 of [TakeutiZaring] p. 88. (Contributed by NM, 27-May-1998.) Avoid ax-pow 5341, ax-un 7745. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0ALT 9025	Shorter proof of en0 9024, depending on ax-pow 5341 and ax-un 7745. (Contributed by NM, 27-May-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
Theorem	en0r 9026	The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024.)
⊢ (∅ ≈ 𝐴 ↔ 𝐴 = ∅)
Theorem	ensn1 9027	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	ensn1g 9028	A singleton is equinumerous to ordinal one. (Contributed by NM, 23-Apr-2004.)
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≈ 1o)
Theorem	enpr1g 9029	{𝐴, 𝐴} has only one element. (Contributed by FL, 15-Feb-2010.)
⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐴} ≈ 1o)
Theorem	en1 9030*	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	en1b 9031	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	reuen1 9032*	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ {𝑥 ∈ 𝐴 ∣ 𝜑} ≈ 1o)
Theorem	euen1 9033	Two ways to express "exactly one". (Contributed by Stefan O'Rear, 28-Oct-2014.)
⊢ (∃!𝑥𝜑 ↔ {𝑥 ∣ 𝜑} ≈ 1o)
Theorem	euen1b 9034*	Two ways to express "𝐴 has a unique element". (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐴 ≈ 1o ↔ ∃!𝑥 𝑥 ∈ 𝐴)
Theorem	funen1cnv 9035	If a function is equinumerous to ordinal 1, then its converse is also a function. (Contributed by BTernaryTau, 8-Oct-2023.)
⊢ ((Fun 𝐹 ∧ 𝐹 ≈ 1o) → Fun ◡𝐹)
Theorem	en1uniel 9036	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	2dom 9037*	A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004.)
⊢ (2o ≼ 𝐴 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦)
Theorem	fundmen 9038	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 9039	A function is equinumerous to its domain. Exercise 4 of [Suppes] p. 98. (Contributed by NM, 17-Sep-2013.)
⊢ ((𝐹 ∈ 𝑉 ∧ Fun 𝐹) → dom 𝐹 ≈ 𝐹)
Theorem	cnven 9040	A relational set is equinumerous to its converse. (Contributed by Mario Carneiro, 28-Dec-2014.)
⊢ ((Rel 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ ◡𝐴)
Theorem	cnvct 9041	If a set is countable, so is its converse. (Contributed by Thierry Arnoux, 29-Dec-2016.)
⊢ (𝐴 ≼ ω → ◡𝐴 ≼ ω)
Theorem	fndmeng 9042	A function is equinumerate to its domain. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐴 ≈ 𝐹)
Theorem	mapsnend 9043	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 9044	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 9045	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 9046	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 9047	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 9048	Two singletons are equinumerous. (Contributed by NM, 9-Nov-2003.) Avoid ax-pow 5341. (Revised by BTernaryTau, 31-Jul-2024.) Avoid ax-un 7745. (Revised by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴} ≈ {𝐵})
Theorem	0fi 9049	The empty set is finite. (Contributed by FL, 14-Jul-2008.) Avoid ax-10 2179, ax-un 7745. (Revised by BTernaryTau, 13-Jan-2025.)
⊢ ∅ ∈ Fin
Theorem	snfi 9050	A singleton is finite. (Contributed by NM, 4-Nov-2002.) (Proof shortened by BTernaryTau, 13-Jan-2025.)
⊢ {𝐴} ∈ Fin
Theorem	fiprc 9051	The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008.)
⊢ Fin ∉ V
Theorem	unen 9052	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 9053	Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg 8990). (Contributed by BTernaryTau, 31-Jul-2024.)
⊢ (𝐴 ∈ ω → 𝐴 ≈ 𝐴)
Theorem	en2prd 9054	Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    ⇒   ⊢ (𝜑 → {𝐴, 𝐵} ≈ {𝐶, 𝐷})
Theorem	enpr2d 9055	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	ssct 9056	Any subset of a countable set is countable. (Contributed by Thierry Arnoux, 31-Jan-2017.) Avoid ax-pow 5341, ax-un 7745. (Revised by BTernaryTau, 7-Dec-2024.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ ω) → 𝐴 ≼ ω)
Theorem	difsnen 9057	All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑋 ∖ {𝐴}) ≈ (𝑋 ∖ {𝐵}))
Theorem	domdifsn 9058	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 9059	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 9060	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 9061	One times a cardinal number. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 × 1o) ≈ 𝐴)
Theorem	endisj 9062*	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 9063	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 5341. (Revised by BTernaryTau, 4-Dec-2024.)
⊢ (((𝐴 ≼ 𝐵 ∧ 𝐶 ≼ 𝐷) ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ∪ 𝐶) ≼ (𝐵 ∪ 𝐷))
Theorem	xpcomf1o 9064*	The canonical bijection from (𝐴 × 𝐵) to (𝐵 × 𝐴). (Contributed by Mario Carneiro, 23-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    ⇒   ⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴)
Theorem	xpcomco 9065*	Composition with the bijection of xpcomf1o 9064 swaps the arguments to a mapping. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥})    &   ⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶)    ⇒   ⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
Theorem	xpcomen 9066	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 9067	Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of [Mendelson] p. 254. (Contributed by NM, 27-Mar-2006.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ≈ (𝐵 × 𝐴))
Theorem	xpsnen2g 9068	A set is equinumerous to its Cartesian product with a singleton on the left. (Contributed by Stefan O'Rear, 21-Nov-2014.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ({𝐴} × 𝐵) ≈ 𝐵)
Theorem	xpassen 9069	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 9070	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 9071	Dominance law for Cartesian product. Theorem 6L(c) of [Enderton] p. 149. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ≼ 𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵))
Theorem	xpdom1g 9072	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 9073	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 9074	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 9075	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 9076*	Lemma for omxpen 9077. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 25-May-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐴 ↦ ((𝐴 ·o 𝑥) +o 𝑦))    ⇒   ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐹:(𝐵 × 𝐴)–1-1-onto→(𝐴 ·o 𝐵))
Theorem	omxpen 9077	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 9078*	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 9079*	Lemma for pw2f1o 9080. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ((𝑆 ∈ 𝒫 𝐴 ∧ 𝐺 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑆, 𝐶, 𝐵))) ↔ (𝐺 ∈ ({𝐵, 𝐶} ↑m 𝐴) ∧ 𝑆 = (◡𝐺 “ {𝐶}))))
Theorem	pw2f1o 9080*	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 9081	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 9082	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 9083	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 9084*	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 9085*	Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ ∪ 𝐷 ⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))))
Theorem	sbthlem2 9086*	Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ ∪ 𝐷)
Theorem	sbthlem3 9087*	Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (ran 𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷))
Theorem	sbthlem4 9088*	Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    ⇒   ⊢ (((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷)))
Theorem	sbthlem5 9089*	Lemma for sbth 9095. (Contributed by NM, 22-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴)
Theorem	sbthlem6 9090*	Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((ran 𝑓 ⊆ 𝐵 ∧ ((dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝐻 = 𝐵)
Theorem	sbthlem7 9091*	Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun 𝑓 ∧ Fun ◡𝑔) → Fun 𝐻)
Theorem	sbthlem8 9092*	Lemma for sbth 9095. (Contributed by NM, 27-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((Fun ◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻)
Theorem	sbthlem9 9093*	Lemma for sbth 9095. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    ⇒   ⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵)
Theorem	sbthlem10 9094*	Lemma for sbth 9095. (Contributed by NM, 28-Mar-1998.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))}    &   ⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbth 9095	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 9085 through sbthlem10 9094; this final piece mainly changes bound variables to eliminate the hypotheses of sbthlem10 9094. 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 9094. This is Metamath 100 proof #25. (Contributed by NM, 8-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵)
Theorem	sbthb 9096	Schroeder-Bernstein Theorem and its converse. (Contributed by NM, 8-Jun-1998.)
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ 𝐴 ≈ 𝐵)
Theorem	sbthcl 9097	Schroeder-Bernstein Theorem in class form. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = ( ≼ ∩ ◡ ≼ )
Theorem	dfsdom2 9098	Alternate definition of strict dominance. Compare Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
⊢ ≺ = ( ≼ ∖ ◡ ≼ )
Theorem	brsdom2 9099	Alternate definition of strict dominance. Definition 3 of [Suppes] p. 97. (Contributed by NM, 27-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴))
Theorem	sdomnsym 9100	Strict dominance is asymmetric. Theorem 21(ii) of [Suppes] p. 97. (Contributed by NM, 8-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴)