P. 88 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elixp 8701*	Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	elixpconst 8702*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	ixpconstg 8703*	Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴))
Theorem	ixpconst 8704*	Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴)
Theorem	ixpeq1 8705*	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ixpeq1d 8706*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ss2ixp 8707	Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2 8708	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dva 8709*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dv 8710*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	cbvixp 8711*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	cbvixpv 8712*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	nfixpw 8713*	Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp 8714 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Gino Giotto, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp 8714	Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 2373. Use the weaker nfixpw 8713 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp1 8715	The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥X𝑥 ∈ 𝐴 𝐵
Theorem	ixpprc 8716*	A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain 𝐴, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.)
⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpf 8717*	A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹:𝐴⟶∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	uniixp 8718*	The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 24-Jun-2015.)
⊢ ∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵)
Theorem	ixpexg 8719*	The existence of an infinite Cartesian product. 𝑥 is normally a free-variable parameter in 𝐵. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 25-Jan-2015.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	ixpin 8720*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpiin 8721*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.)
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpint 8722*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦)
Theorem	ixp0x 8723	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
⊢ X𝑥 ∈ ∅ 𝐴 = {∅}
Theorem	ixpssmap2g 8724*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 8725 avoids ax-rep 5210. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴))
Theorem	ixpssmapg 8725*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴))
Theorem	0elixp 8726	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴
Theorem	ixpn0 8727	The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 10248. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ (X𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀𝑥 ∈ 𝐴 𝐵 ≠ ∅)
Theorem	ixp0 8728	The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 10248. (Contributed by NM, 1-Oct-2006.) (Proof shortened by Mario Carneiro, 22-Jun-2016.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpssmap 8729*	An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)
Theorem	resixp 8730*	Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.)
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐶) → (𝐹 ↾ 𝐵) ∈ X𝑥 ∈ 𝐵 𝐶)
Theorem	undifixp 8731*	Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.)
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶)
Theorem	mptelixpg 8732*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
Theorem	resixpfo 8733*	Restriction of elements of an infinite Cartesian product creates a surjection, if the original Cartesian product is nonempty. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝐹 = (𝑓 ∈ X𝑥 ∈ 𝐴 𝐶 ↦ (𝑓 ↾ 𝐵))    ⇒   ⊢ ((𝐵 ⊆ 𝐴 ∧ X𝑥 ∈ 𝐴 𝐶 ≠ ∅) → 𝐹:X𝑥 ∈ 𝐴 𝐶–onto→X𝑥 ∈ 𝐵 𝐶)
Theorem	elixpsn 8734*	Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {⟨𝐴, 𝑦⟩}))
Theorem	ixpsnf1o 8735*	A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥}))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐹:𝐴–1-1-onto→X𝑦 ∈ {𝐼}𝐴)
Theorem	mapsnf1o 8736*	A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥}))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑m {𝐼}))
Theorem	boxriin 8737*	A rectangular subset of a rectangular set can be recovered as the relative intersection of single-axis restrictions. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (∀𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → X𝑥 ∈ 𝐼 𝐴 = (X𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐴, 𝐵)))
Theorem	boxcutc 8738*	The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) = X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵))
2.4.25  Equinumerosity
Syntax	cen 8739	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ≈
Syntax	cdom 8740	Extend class definition to include the dominance relation (curly "less than or equal to")
class ≼
Syntax	csdm 8741	Extend class definition to include the strict dominance relation (curly less-than)
class ≺
Syntax	cfn 8742	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 8743*	Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ≈ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 8752. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
Definition	df-dom 8744*	Define the dominance relation. For an alternate definition see dfdom2 8775. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 8759 and domen 8760. (Contributed by NM, 28-Mar-1998.)
⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
Definition	df-sdom 8745	Define the strict dominance relation. Alternate possible definitions are derived as brsdom 8772 and brsdom2 8893. Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
⊢ ≺ = ( ≼ ∖ ≈ )
Definition	df-fin 8746*	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 9408. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (Theorem isfinite 9419.) (Contributed by NM, 22-Aug-2008.)
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
Theorem	relen 8747	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≈
Theorem	reldom 8748	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≼
Theorem	relsdom 8749	Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.)
⊢ Rel ≺
Theorem	encv 8750	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	breng 8751*	Equinumerosity relation. This variation of bren 8752 does not require the Axiom of Union. (Contributed by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
Theorem	bren 8752*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) (Proof shortened by BTernaryTau, 23-Sep-2024.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)
Theorem	brenOLD 8753*	Obsolete version of bren 8752 as of 23-Sep-2024. (Contributed by NM, 15-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)
Theorem	brdom2g 8754*	Dominance relation. This variation of brdomg 8755 does not require the Axiom of Union. (Contributed by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomg 8755*	Dominance relation. (Contributed by NM, 15-Jun-1998.) (Proof shortened by BTernaryTau, 29-Nov-2024.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomgOLD 8756*	Obsolete version of brdomg 8755 as of 29-Nov-2024. (Contributed by NM, 15-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomi 8757*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7597. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	brdomiOLD 8758*	Obsolete version of brdomi 8757 as of 29-Nov-2024. (Contributed by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	brdom 8759*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	domen 8760*	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	domeng 8761*	Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146. (Contributed by NM, 24-Apr-2004.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)))
Theorem	ctex 8762	A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
Theorem	f1oen3g 8763	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 8768 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom3g 8764	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 8769 does not require the Axiom of Replacement nor the Axiom of Power Sets. (Contributed by BTernaryTau, 9-Sep-2024.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oen2g 8765	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 8768 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom2g 8766	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 8769 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.) (Proof shortened by BTernaryTau, 25-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1dom2gOLD 8767	Obsolete version of f1dom2g 8766 as of 25-Sep-2024. (Contributed by Mario Carneiro, 24-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oeng 8768	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1domg 8769	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵))
Theorem	f1oen 8770	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 8771	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)
Theorem	brsdom 8772	Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))
Theorem	isfi 8773*	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 8774	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
⊢ ≈ ⊆ ≼
Theorem	dfdom2 8775	Alternate definition of dominance. (Contributed by NM, 17-Jun-1998.)
⊢ ≼ = ( ≺ ∪ ≈ )
Theorem	endom 8776	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94. (Contributed by NM, 28-May-1998.)
⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomdom 8777	Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵)
Theorem	sdomnen 8778	Strict dominance implies non-equinumerosity. (Contributed by NM, 10-Jun-1998.)
⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
Theorem	brdom2 8779	Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.)
⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
Theorem	bren2 8780	Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.)
⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))
Theorem	enrefg 8781	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴)
Theorem	enref 8782	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ≈ 𝐴
Theorem	eqeng 8783	Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵))
Theorem	domrefg 8784	Dominance is reflexive. (Contributed by NM, 18-Jun-1998.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≼ 𝐴)
Theorem	en2d 8785*	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 8786*	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 8787*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ V)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ V)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐷))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	en3i 8788*	Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 19-Jul-2004.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐵)    &   ⊢ (𝑦 ∈ 𝐵 → 𝐷 ∈ 𝐴)    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑥 = 𝐷 ↔ 𝑦 = 𝐶))    ⇒   ⊢ 𝐴 ≈ 𝐵
Theorem	dom2lem 8789*	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 8790*	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 8791*	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 8792*	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 8793*	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 8794	Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)
⊢ I ⊆ ≈
Theorem	ssdomg 8795	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 8796	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 8797	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
Theorem	ensym 8798	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
Theorem	ensymi 8799	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.)
⊢ 𝐴 ≈ 𝐵    ⇒   ⊢ 𝐵 ≈ 𝐴
Theorem	ensymd 8800	Symmetry of equinumerosity. Deduction form of ensym 8798. (Contributed by David Moews, 1-May-2017.)
⊢ (𝜑 → 𝐴 ≈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 ≈ 𝐴)