P. 89 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 8801-8900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fset0 8801	The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.)
⊢ {𝑓 ∣ 𝑓:∅⟶𝐵} = {∅}
Theorem	fsetdmprc0 8802*	The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.)
⊢ (𝐴 ∉ V → {𝑓 ∣ 𝑓 Fn 𝐴} = ∅)
Theorem	fsetex 8803*	The set of functions between two classes exists if the codomain exists. Generalization of mapex 7892 to arbitrary domains. (Contributed by AV, 14-Aug-2024.)
⊢ (𝐵 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V)
Theorem	f1setex 8804*	The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024.)
⊢ (𝐵 ∈ 𝑉 → {𝑓 ∣ 𝑓:𝐴–1-1→𝐵} ∈ V)
Theorem	fosetex 8805*	The set of surjections between two classes exists (without any precondition). (Contributed by AV, 8-Aug-2024.)
⊢ {𝑓 ∣ 𝑓:𝐴–onto→𝐵} ∈ V
Theorem	f1osetex 8806*	The set of bijections between two classes exists. (Contributed by AV, 30-Mar-2024.) (Revised by AV, 8-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.)
⊢ {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐵} ∈ V
Theorem	fsetfcdm 8807*	The class of functions with a given domain and a given codomain is mapped, through evaluation at a point of the domain, into the codomain. (Contributed by AV, 15-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ 𝑓:𝐴⟶𝐵}    &   ⊢ 𝑆 = (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋))    ⇒   ⊢ (𝑋 ∈ 𝐴 → 𝑆:𝐹⟶𝐵)
Theorem	fsetfocdm 8808*	The class of functions with a given domain that is a set and a given codomain is mapped, through evaluation at a point of the domain, onto the codomain. (Contributed by AV, 15-Sep-2024.)
⊢ 𝐹 = {𝑓 ∣ 𝑓:𝐴⟶𝐵}    &   ⊢ 𝑆 = (𝑔 ∈ 𝐹 ↦ (𝑔‘𝑋))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → 𝑆:𝐹–onto→𝐵)
Theorem	fsetprcnex 8809*	The class of all functions from a nonempty set 𝐴 into a proper class 𝐵 is not a set. If one of the preconditions is not fufilled, then {𝑓 ∣ 𝑓:𝐴⟶𝐵} is a set, see fsetdmprc0 8802 for 𝐴 ∉ V, fset0 8801 for 𝐴 = ∅, and fsetex 8803 for 𝐵 ∈ V, see also fsetexb 8811. (Contributed by AV, 14-Sep-2024.) (Proof shortened by BJ, 15-Sep-2024.)
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) ∧ 𝐵 ∉ V) → {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∉ V)
Theorem	fsetcdmex 8810*	The class of all functions from a nonempty set 𝐴 into a class 𝐵 is a set iff 𝐵 is a set . (Contributed by AV, 15-Sep-2024.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → (𝐵 ∈ V ↔ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V))
Theorem	fsetexb 8811*	The class of all functions from a class 𝐴 into a class 𝐵 is a set iff 𝐵 is a set or 𝐴 is not a set or 𝐴 is empty. (Contributed by AV, 15-Sep-2024.)
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V ↔ (𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V))
Theorem	elmapfn 8812	A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶)
Theorem	elmapfun 8813	A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → Fun 𝐴)
Theorem	elmapssres 8814	A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ ((𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷))
Theorem	elmapssresd 8815	A restricted mapping is a mapping. EDITORIAL: Could be used to shorten elpm2r 8792 with some reordering involving mapsspm 8824. (Contributed by SN, 11-Mar-2025.)
⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m 𝐶))    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷))
Theorem	fpmg 8816	A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴))
Theorem	pmss12g 8817	Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷))
Theorem	pmresg 8818	Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵))
Theorem	elmap 8819	Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)
Theorem	mapval2 8820*	Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑m 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵})
Theorem	elpm 8821	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 8822	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 8823	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 8824	Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ (𝐴 ↑m 𝐵) ⊆ (𝐴 ↑pm 𝐵)
Theorem	pmsspw 8825	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 8826	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.)
⊢ (𝐴 ↑m 𝐵) ⊆ 𝒫 (𝐵 × 𝐴)
Theorem	mapfvd 8827	The value of a function that maps from 𝐵 to 𝐴. (Contributed by AV, 2-Feb-2023.)
⊢ 𝑀 = (𝐴 ↑m 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑀)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐴)
Theorem	elmapresaun 8828	fresaun 6711 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵)))
Theorem	fvmptmap 8829*	Special case of fvmpt 6947 for operator theorems. (Contributed by NM, 27-Nov-2007.)
⊢ 𝐶 ∈ V    &   ⊢ 𝐷 ∈ V    &   ⊢ 𝑅 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    &   ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑m 𝐷) ↦ 𝐵)    ⇒   ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶)
Theorem	map0e 8830	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.) (Proof shortened by AV, 14-Jul-2022.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑m ∅) = 1o)
Theorem	map0b 8831	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.)
⊢ (𝐴 ≠ ∅ → (∅ ↑m 𝐴) = ∅)
Theorem	map0g 8832	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.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅)))
Theorem	0map0sn0 8833	The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024.)
⊢ (∅ ↑m ∅) = {∅}
Theorem	mapsnd 8834*	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.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}})
Theorem	map0 8835	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    ⇒   ⊢ ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅))
Theorem	mapsn 8836*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {⟨𝐵, 𝑦⟩}}
Theorem	mapss 8837	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶))
Theorem	fdiagfn 8838*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼))
Theorem	fvdiagfn 8839*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋}))
Theorem	mapsnconst 8840	Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    ⇒   ⊢ (𝐹 ∈ (𝐵 ↑m 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)}))
Theorem	mapsncnv 8841*	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    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))
Theorem	mapsnf1o2 8842*	Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋))    ⇒   ⊢ 𝐹:(𝐵 ↑m 𝑆)–1-1-onto→𝐵
Theorem	mapsnf1o3 8843*	Explicit bijection in the reverse of mapsnf1o2 8842. (Contributed by Stefan O'Rear, 24-Mar-2015.)
⊢ 𝑆 = {𝑋}    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦}))    ⇒   ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑m 𝑆)
Theorem	ralxpmap 8844*	Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.)
⊢ (𝑓 = (𝑔 ∪ {⟨𝐽, 𝑦⟩}) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓))
2.4.28  Infinite Cartesian products
Syntax	cixp 8845	Extend class notation to include infinite Cartesian products.
class X𝑥 ∈ 𝐴 𝐵
Definition	df-ixp 8846*	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 8847*	Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 8846, 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 8848*	The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.)
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)})
Theorem	elixp2 8849*	Membership in an infinite Cartesian product. See df-ixp 8846 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	fvixp 8850*	Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷)    ⇒   ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷)
Theorem	ixpfn 8851*	A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.)
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴)
Theorem	elixp 8852*	Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
Theorem	elixpconst 8853*	Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.)
⊢ 𝐹 ∈ V    ⇒   ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵)
Theorem	ixpconstg 8854*	Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴))
Theorem	ixpconst 8855*	Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴)
Theorem	ixpeq1 8856*	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ixpeq1d 8857*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶)
Theorem	ss2ixp 8858	Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2 8859	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dva 8860*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpeq2dv 8861*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
⊢ (𝜑 → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	cbvixp 8862*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    &   ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	cbvixpv 8863*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶
Theorem	nfixpw 8864*	Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp 8865 with a disjoint variable condition, which does not require ax-13 2376. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2376. (Revised by GG, 26-Jan-2024.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp 8865	Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 2376. Use the weaker nfixpw 8864 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵
Theorem	nfixp1 8866	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 8867*	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 8868*	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 8869*	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 8870*	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 8871*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpiin 8872*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.)
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶)
Theorem	ixpint 8873*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦)
Theorem	ixp0x 8874	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
⊢ X𝑥 ∈ ∅ 𝐴 = {∅}
Theorem	ixpssmap2g 8875*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 8876 avoids ax-rep 5212. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴))
Theorem	ixpssmapg 8876*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴))
Theorem	0elixp 8877	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴
Theorem	ixpn0 8878	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 10405. (Contributed by Mario Carneiro, 22-Jun-2016.)
⊢ (X𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀𝑥 ∈ 𝐴 𝐵 ≠ ∅)
Theorem	ixp0 8879	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 10405. (Contributed by NM, 1-Oct-2006.) (Proof shortened by Mario Carneiro, 22-Jun-2016.)
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅)
Theorem	ixpssmap 8880*	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 8881*	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 8882*	Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.)
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶)
Theorem	mptelixpg 8883*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾))
Theorem	resixpfo 8884*	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 8885*	Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {⟨𝐴, 𝑦⟩}))
Theorem	ixpsnf1o 8886*	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 8887*	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 8888*	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 8889*	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.29  Equinumerosity
Syntax	cen 8890	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ≈
Syntax	cdom 8891	Extend class definition to include the dominance relation (curly "less than or equal to")
class ≼
Syntax	csdm 8892	Extend class definition to include the strict dominance relation (curly less-than)
class ≺
Syntax	cfn 8893	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 8894*	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 8903. (Contributed by NM, 28-Mar-1998.)
⊢ ≈ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦}
Definition	df-dom 8895*	Define the dominance relation. For an alternate definition see dfdom2 8925. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 8907 and domen 8908. (Contributed by NM, 28-Mar-1998.)
⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
Definition	df-sdom 8896	Define the strict dominance relation. Alternate possible definitions are derived as brsdom 8921 and brsdom2 9039. Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
⊢ ≺ = ( ≼ ∖ ≈ )
Definition	df-fin 8897*	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 9562. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (Theorem isfinite 9573.) (Contributed by NM, 22-Aug-2008.)
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦}
Theorem	relen 8898	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≈
Theorem	reldom 8899	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
⊢ Rel ≼
Theorem	relsdom 8900	Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.)
⊢ Rel ≺