P. 70 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6901-7000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pmfun 6901	A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) → Fun 𝐹)
Theorem	elmapex 6902	Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
Theorem	elmapi 6903	A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴:𝐶⟶𝐵)
Theorem	elmapfn 6904	A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → 𝐴 Fn 𝐶)
Theorem	elmapfun 6905	A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (𝐴 ∈ (𝐵 ↑𝑚 𝐶) → Fun 𝐴)
Theorem	elmapssres 6906	A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝐴 ∈ (𝐵 ↑𝑚 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑𝑚 𝐷))
Theorem	fpmg 6907	A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴))
Theorem	pmss12g 6908	Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷))
Theorem	pmresg 6909	Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵))
Theorem	elmap 6910	Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐴)
Theorem	mapval2 6911*	Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑𝑚 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵})
Theorem	elpm 6912	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (𝐵 × 𝐴)))
Theorem	elpm2 6913	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵))
Theorem	fpm 6914	A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ∈ (𝐵 ↑pm 𝐴))
Theorem	mapsspm 6915	Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ (𝐴 ↑𝑚 𝐵) ⊆ (𝐴 ↑pm 𝐵)
Theorem	pmsspw 6916	Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ (𝐴 ↑pm 𝐵) ⊆ 𝒫 (𝐵 × 𝐴)
Theorem	mapsspw 6917	Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ↑𝑚 𝐵) ⊆ 𝒫 (𝐵 × 𝐴)
Theorem	fvmptmap 6918*	Special case of fvmpt 5753 for operator theorems. (Contributed by NM, 27-Nov-2007.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝑅 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑𝑚 𝐷) ↦ 𝐵)    ⇒   ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶)
Theorem	map0e 6919	Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑𝑚 ∅) = 1o)
Theorem	map0b 6920	Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≠ ∅ → (∅ ↑𝑚 𝐴) = ∅)
Theorem	map0g 6921	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑𝑚 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅)))
Theorem	mapsnd 6922*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}})
Theorem	map0 6923	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐴 ↑𝑚 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅))
Theorem	mapsn 6924*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑𝑚 {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
Theorem	mapss 6925	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑𝑚 𝐶) ⊆ (𝐵 ↑𝑚 𝐶))
Theorem	fdiagfn 6926*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑𝑚 𝐼))
Theorem	fvdiagfn 6927*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋}))
Theorem	mapsnconst 6928	Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐵 ↑𝑚 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)}))
Theorem	mapsncnv 6929*	Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))
Theorem	mapsnf1o2 6930*	Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑𝑚 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ 𝐹:(𝐵 ↑𝑚 𝑆)–1-1-onto→𝐵
Theorem	mapsnf1o3 6931*	Explicit bijection in the reverse of mapsnf1o2 6930. (Contributed by Stefan O'Rear, 24-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))    ⇒   ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑𝑚 𝑆)
2.6.28  Infinite Cartesian products
Syntax	cixp 6932	Extend class notation to include infinite Cartesian products.
class X𝑥 ∈ 𝐴 𝐵
Definition	df-ixp 6933*	Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥 ∈ 𝐴 written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
Theorem	dfixp 6934*	Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 6933, under the assumption that 𝐴 and 𝑥 are disjoint. This way, we can say that 𝑥 is bound in X𝑥 ∈ 𝐴𝐵 even if it appears free in 𝐴. (Contributed by Mario Carneiro, 12-Aug-2016.)
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
Theorem	ixpsnval 6935*	The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.)
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)})
Theorem	elixp2 6936*	Membership in an infinite Cartesian product. See df-ixp 6933 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fvixp 6937*	Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷)
Theorem	ixpfn 6938*	A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴)
Theorem	elixp 6939*	Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	elixpconst 6940*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	ixpconstg 6941*	Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴))
Theorem	ixpconst 6942*	Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑𝑚 𝐴)
Theorem	ixpeq1 6943*	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ixpeq1d 6944*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ss2ixp 6945	Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2 6946	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dva 6947*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dv 6948*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	cbvixp 6949*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	cbvixpv 6950*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	nfixpxy 6951*	Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp1 6952	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 6953*	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 6954*	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 6955*	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	ixpexgg 6956*	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 Jim Kingdon, 15-Feb-2023.)
⊢ ((𝐴 ∈ 𝑊 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → X𝑥 ∈ 𝐴 𝐵 ∈ V)
Theorem	ixpin 6957*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpiinm 6958*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ (∃𝑧 𝑧 ∈ 𝐵 → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpintm 6959*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
⊢ (∃𝑧 𝑧 ∈ 𝐵 → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦)
Theorem	ixp0x 6960	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
⊢ X𝑥 ∈ ∅ 𝐴 = {∅}
Theorem	ixpssmap2g 6961*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 6962 avoids ax-coll 4224. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴))
Theorem	ixpssmapg 6962*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴))
Theorem	0elixp 6963	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴
Theorem	ixpm 6964*	If an infinite Cartesian product of a family 𝐵(𝑥) is inhabited, every 𝐵(𝑥) is inhabited. (Contributed by Mario Carneiro, 22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
⊢ (∃𝑓 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵 → ∀𝑥 ∈ 𝐴 ∃𝑧 𝑧 ∈ 𝐵)
Theorem	ixp0 6965	The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim Kingdon, 16-Feb-2023.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpssmap 6966*	An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)
Theorem	resixp 6967*	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	mptelixpg 6968*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
Theorem	elixpsn 6969*	Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {⟨𝐴, 𝑦⟩}))
Theorem	ixpsnf1o 6970*	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 6971*	A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥}))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑𝑚 {𝐼}))
2.6.29  Equinumerosity
Syntax	cen 6972	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ≈
Syntax	cdom 6973	Extend class definition to include the dominance relation (curly less-than-or-equal)
class ≼
Syntax	cfn 6974	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 6975*	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 6982. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
Definition	df-dom 6976*	Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6986 and domen 6987. (Contributed by NM, 28-Mar-1998.)
⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
Definition	df-fin 6977*	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 16733. (Contributed by NM, 22-Aug-2008.)
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
Theorem	relen 6978	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≈
Theorem	reldom 6979	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≼
Theorem	encv 6980	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
Theorem	breng 6981*	Equinumerosity relation. This variation of bren 6982 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 6982. (Revised by BTernaryTau, 23-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵))
Theorem	bren 6982*	Equinumerosity relation. (Contributed by NM, 15-Jun-1998.)
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)
Theorem	brdom2g 6983*	Dominance relation. This variation of brdomg 6984 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 6984. (Revised by BTernaryTau, 29-Nov-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomg 6984*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵))
Theorem	brdomi 6985*	Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.)
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	brdom 6986*	Dominance relation. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)
Theorem	domen 6987*	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵))
Theorem	domeng 6988*	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 6989	A class dominated by ω is a set. See also ctfoex 7408 which says that a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.)
⊢ (𝐴 ≼ ω → 𝐴 ∈ V)
Theorem	f1oen4g 6990	The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 6995 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom4g 6991	The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 6996 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.)
⊢ (((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oen3g 6992	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6995 does not require the Axiom of Replacement. (Contributed by NM, 13-Jan-2007.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1oen2g 6993	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 6995 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1dom2g 6994	The domain of a one-to-one function is dominated by its codomain. This variation of f1domg 6996 does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → 𝐴 ≼ 𝐵)
Theorem	f1oeng 6995	The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
Theorem	f1domg 6996	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004.)
⊢ (𝐵 ∈ 𝐶 → (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵))
Theorem	f1oen 6997	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 6998	The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 19-Jun-1998.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐴 ≼ 𝐵)
Theorem	isfi 6999*	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 7000	Equinumerosity implies dominance. (Contributed by NM, 31-Mar-1998.)
⊢ ≈ ⊆ ≼