P. 68 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ecovidi 6701*	Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. M , N >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( M e. S /\ N e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. M , N >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. z , w >. ] .~ ) = [ <. W , X >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. x , y >. ] .~ .x. [ <. v , u >. ] .~ ) = [ <. Y , Z >. ] .~ )   &    |- ( ( ( W e. S /\ X e. S ) /\ ( Y e. S /\ Z e. S ) ) -> ( [ <. W , X >. ] .~ .+ [ <. Y , Z >. ] .~ ) = [ <. K , L >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( M e. S /\ N e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( W e. S /\ X e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( v e. S /\ u e. S ) ) -> ( Y e. S /\ Z e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> H = K )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> J = L )   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( A .x. ( B .+ C ) ) = ( ( A .x. B ) .+ ( A .x. C ) ) )
2.6.26  The mapping operation
Syntax	cmap 6702	Extend the definition of a class to include the mapping operation. (Read for A ^m B, "the set of all functions that map from B to A.)
class ^m
Syntax	cpm 6703	Extend the definition of a class to include the partial mapping operation. (Read for A ^pm B, "the set of all partial functions that map from B to A.)
class ^pm
Definition	df-map 6704*	Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written ( A ^m B ) (see mapval 6714). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g., Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read " A pre B " (e.g., definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map( B, A) for our ( A ^m B ). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. (Contributed by NM, 8-Dec-2003.)
|- ^m = ( x e. _V , y e. _V |-> { f | f : y --> x } )
Definition	df-pm 6705*	Define the partial mapping operation. A partial function from B to A is a function from a subset of B to A. The set of all partial functions from B to A is written ( A ^pm B ) (see pmvalg 6713). A notation for this operation apparently does not appear in the literature. We use ^pm to distinguish it from the less general set exponentiation operation ^m (df-map 6704) . See mapsspm 6736 for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007.)
|- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
Theorem	mapprc 6706*	When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of [Mendelson] p. 255. (Contributed by NM, 8-Dec-2003.)
|- ( -. A e. _V -> { f | f : A --> B } = (/) )
Theorem	pmex 6707*	The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007.)
|- ( ( A e. C /\ B e. D ) -> { f | ( Fun f /\ f C_ ( A X. B ) ) } e. _V )
Theorem	mapex 6708*	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.)
|- ( ( A e. C /\ B e. D ) -> { f | f : A --> B } e. _V )
Theorem	fnmap 6709	Set exponentiation has a universal domain. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ^m Fn ( _V X. _V )
Theorem	fnpm 6710	Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ^pm Fn ( _V X. _V )
Theorem	reldmmap 6711	Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- Rel dom ^m
Theorem	mapvalg 6712*	The value of set exponentiation. ( A ^m B ) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. C /\ B e. D ) -> ( A ^m B ) = { f | f : B --> A } )
Theorem	pmvalg 6713*	The value of the partial mapping operation. ( A ^pm B ) is the set of all partial functions that map from B to A. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. C /\ B e. D ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } )
Theorem	mapval 6714*	The value of set exponentiation (inference version). ( A ^m B ) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. (Contributed by NM, 8-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m B ) = { f | f : B --> A }
Theorem	elmapg 6715	Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^m B ) <-> C : B --> A ) )
Theorem	elmapd 6716	Deduction form of elmapg 6715. (Contributed by BJ, 11-Apr-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( C e. ( A ^m B ) <-> C : B --> A ) )
Theorem	mapdm0 6717	The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.) (Proof shortened by Thierry Arnoux, 3-Dec-2021.)
|- ( B e. V -> ( B ^m (/) ) = { (/) } )
Theorem	elpmg 6718	The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) )
Theorem	elpm2g 6719	The predicate "is a partial function". (Contributed by NM, 31-Dec-2013.)
|- ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )
Theorem	elpm2r 6720	Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013.)
|- ( ( ( A e. V /\ B e. W ) /\ ( F : C --> A /\ C C_ B ) ) -> F e. ( A ^pm B ) )
Theorem	elpmi 6721	A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015.)
|- ( F e. ( A ^pm B ) -> ( F : dom F --> A /\ dom F C_ B ) )
Theorem	pmfun 6722	A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( F e. ( A ^pm B ) -> Fun F )
Theorem	elmapex 6723	Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( A e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) )
Theorem	elmapi 6724	A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. ( B ^m C ) -> A : C --> B )
Theorem	elmapfn 6725	A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)
|- ( A e. ( B ^m C ) -> A Fn C )
Theorem	elmapfun 6726	A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- ( A e. ( B ^m C ) -> Fun A )
Theorem	elmapssres 6727	A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|- ( ( A e. ( B ^m C ) /\ D C_ C ) -> ( A |` D ) e. ( B ^m D ) )
Theorem	fpmg 6728	A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ( A e. V /\ B e. W /\ F : A --> B ) -> F e. ( B ^pm A ) )
Theorem	pmss12g 6729	Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ( ( A C_ C /\ B C_ D ) /\ ( C e. V /\ D e. W ) ) -> ( A ^pm B ) C_ ( C ^pm D ) )
Theorem	pmresg 6730	Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ( B e. V /\ F e. ( A ^pm C ) ) -> ( F |` B ) e. ( A ^pm B ) )
Theorem	elmap 6731	Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( F e. ( A ^m B ) <-> F : B --> A )
Theorem	mapval2 6732*	Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m B ) = ( ~P ( B X. A ) i^i { f | f Fn B } )
Theorem	elpm 6733	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( F e. ( A ^pm B ) <-> ( Fun F /\ F C_ ( B X. A ) ) )
Theorem	elpm2 6734	The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) )
Theorem	fpm 6735	A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.)
|- A e. _V   &    |- B e. _V   =>    |- ( F : A --> B -> F e. ( B ^pm A ) )
Theorem	mapsspm 6736	Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.)
|- ( A ^m B ) C_ ( A ^pm B )
Theorem	pmsspw 6737	Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( A ^pm B ) C_ ~P ( B X. A )
Theorem	mapsspw 6738	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.)
|- ( A ^m B ) C_ ~P ( B X. A )
Theorem	fvmptmap 6739*	Special case of fvmpt 5634 for operator theorems. (Contributed by NM, 27-Nov-2007.)
|- C e. _V   &    |- D e. _V   &    |- R e. _V   &    |- ( x = A -> B = C )   &    |- F = ( x e. ( R ^m D ) |-> B )   =>    |- ( A : D --> R -> ( F ` A ) = C )
Theorem	map0e 6740	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.)
|- ( A e. V -> ( A ^m (/) ) = 1o )
Theorem	map0b 6741	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.)
|- ( A =/= (/) -> ( (/) ^m A ) = (/) )
Theorem	map0g 6742	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.)
|- ( ( A e. V /\ B e. W ) -> ( ( A ^m B ) = (/) <-> ( A = (/) /\ B =/= (/) ) ) )
Theorem	map0 6743	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.)
|- A e. _V   &    |- B e. _V   =>    |- ( ( A ^m B ) = (/) <-> ( A = (/) /\ B =/= (/) ) )
Theorem	mapsn 6744*	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.)
|- A e. _V   &    |- B e. _V   =>    |- ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } }
Theorem	mapss 6745	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)
|- ( ( B e. V /\ A C_ B ) -> ( A ^m C ) C_ ( B ^m C ) )
Theorem	fdiagfn 6746*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. B |-> ( I X. { x } ) )   =>    |- ( ( B e. V /\ I e. W ) -> F : B --> ( B ^m I ) )
Theorem	fvdiagfn 6747*	Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. B |-> ( I X. { x } ) )   =>    |- ( ( I e. W /\ X e. B ) -> ( F ` X ) = ( I X. { X } ) )
Theorem	mapsnconst 6748	Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.)
|- S = { X }   &    |- B e. _V   &    |- X e. _V   =>    |- ( F e. ( B ^m S ) -> F = ( S X. { ( F ` X ) } ) )
Theorem	mapsncnv 6749*	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.)
|- S = { X }   &    |- B e. _V   &    |- X e. _V   &    |- F = ( x e. ( B ^m S ) |-> ( x ` X ) )   =>    |- `' F = ( y e. B |-> ( S X. { y } ) )
Theorem	mapsnf1o2 6750*	Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.)
|- S = { X }   &    |- B e. _V   &    |- X e. _V   &    |- F = ( x e. ( B ^m S ) |-> ( x ` X ) )   =>    |- F : ( B ^m S ) -1-1-onto-> B
Theorem	mapsnf1o3 6751*	Explicit bijection in the reverse of mapsnf1o2 6750. (Contributed by Stefan O'Rear, 24-Mar-2015.)
|- S = { X }   &    |- B e. _V   &    |- X e. _V   &    |- F = ( y e. B |-> ( S X. { y } ) )   =>    |- F : B -1-1-onto-> ( B ^m S )
2.6.27  Infinite Cartesian products
Syntax	cixp 6752	Extend class notation to include infinite Cartesian products.
class X_ x e. A B
Definition	df-ixp 6753*	Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with x e. A 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 B represents a class expression containing x free and thus can be thought of as B ( x ). Normally, x is not free in A, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.)
|- X_ x e. A B = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. B ) }
Theorem	dfixp 6754*	Eliminate the expression { x | x e. A } in df-ixp 6753, under the assumption that A and x are disjoint. This way, we can say that x is bound in X_ x e. A B even if it appears free in A. (Contributed by Mario Carneiro, 12-Aug-2016.)
|- X_ x e. A B = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }
Theorem	ixpsnval 6755*	The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.)
|- ( X e. V -> X_ x e. { X } B = { f | ( f Fn { X } /\ ( f ` X ) e. [_ X / x ]_ B ) } )
Theorem	elixp2 6756*	Membership in an infinite Cartesian product. See df-ixp 6753 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)
|- ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
Theorem	fvixp 6757*	Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( x = C -> B = D )   =>    |- ( ( F e. X_ x e. A B /\ C e. A ) -> ( F ` C ) e. D )
Theorem	ixpfn 6758*	A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.)
|- ( F e. X_ x e. A B -> F Fn A )
Theorem	elixp 6759*	Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
|- F e. _V   =>    |- ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
Theorem	elixpconst 6760*	Membership in an infinite Cartesian product of a constant B. (Contributed by NM, 12-Apr-2008.)
|- F e. _V   =>    |- ( F e. X_ x e. A B <-> F : A --> B )
Theorem	ixpconstg 6761*	Infinite Cartesian product of a constant B. (Contributed by Mario Carneiro, 11-Jan-2015.)
|- ( ( A e. V /\ B e. W ) -> X_ x e. A B = ( B ^m A ) )
Theorem	ixpconst 6762*	Infinite Cartesian product of a constant B. (Contributed by NM, 28-Sep-2006.)
|- A e. _V   &    |- B e. _V   =>    |- X_ x e. A B = ( B ^m A )
Theorem	ixpeq1 6763*	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
|- ( A = B -> X_ x e. A C = X_ x e. B C )
Theorem	ixpeq1d 6764*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> X_ x e. A C = X_ x e. B C )
Theorem	ss2ixp 6765	Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
|- ( A. x e. A B C_ C -> X_ x e. A B C_ X_ x e. A C )
Theorem	ixpeq2 6766	Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.)
|- ( A. x e. A B = C -> X_ x e. A B = X_ x e. A C )
Theorem	ixpeq2dva 6767*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ( ph /\ x e. A ) -> B = C )   =>    |- ( ph -> X_ x e. A B = X_ x e. A C )
Theorem	ixpeq2dv 6768*	Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.)
|- ( ph -> B = C )   =>    |- ( ph -> X_ x e. A B = X_ x e. A C )
Theorem	cbvixp 6769*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.)
|- F/_ y B   &    |- F/_ x C   &    |- ( x = y -> B = C )   =>    |- X_ x e. A B = X_ y e. A C
Theorem	cbvixpv 6770*	Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( x = y -> B = C )   =>    |- X_ x e. A B = X_ y e. A C
Theorem	nfixpxy 6771*	Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- F/_ y A   &    |- F/_ y B   =>    |- F/_ y X_ x e. A B
Theorem	nfixp1 6772	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.)
|- F/_ x X_ x e. A B
Theorem	ixpprc 6773*	A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain A, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.)
|- ( -. A e. _V -> X_ x e. A B = (/) )
Theorem	ixpf 6774*	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.)
|- ( F e. X_ x e. A B -> F : A --> U_ x e. A B )
Theorem	uniixp 6775*	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.)
|- U. X_ x e. A B C_ ( A X. U_ x e. A B )
Theorem	ixpexgg 6776*	The existence of an infinite Cartesian product. x is normally a free-variable parameter in B. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- ( ( A e. W /\ A. x e. A B e. V ) -> X_ x e. A B e. _V )
Theorem	ixpin 6777*	The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.)
|- X_ x e. A ( B i^i C ) = ( X_ x e. A B i^i X_ x e. A C )
Theorem	ixpiinm 6778*	The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- ( E. z z e. B -> X_ x e. A |^|_ y e. B C = |^|_ y e. B X_ x e. A C )
Theorem	ixpintm 6779*	The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.)
|- ( E. z z e. B -> X_ x e. A |^| B = |^|_ y e. B X_ x e. A y )
Theorem	ixp0x 6780	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
|- X_ x e. (/) A = { (/) }
Theorem	ixpssmap2g 6781*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 6782 avoids ax-coll 4144. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( U_ x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
Theorem	ixpssmapg 6782*	An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.)
|- ( A. x e. A B e. V -> X_ x e. A B C_ ( U_ x e. A B ^m A ) )
Theorem	0elixp 6783	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
|- (/) e. X_ x e. (/) A
Theorem	ixpm 6784*	If an infinite Cartesian product of a family B ( x ) is inhabited, every B ( x ) is inhabited. (Contributed by Mario Carneiro, 22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.)
|- ( E. f f e. X_ x e. A B -> A. x e. A E. z z e. B )
Theorem	ixp0 6785	The infinite Cartesian product of a family B ( x ) with an empty member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim Kingdon, 16-Feb-2023.)
|- ( E. x e. A B = (/) -> X_ x e. A B = (/) )
Theorem	ixpssmap 6786*	An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.)
|- B e. _V   =>    |- X_ x e. A B C_ ( U_ x e. A B ^m A )
Theorem	resixp 6787*	Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.)
|- ( ( B C_ A /\ F e. X_ x e. A C ) -> ( F |` B ) e. X_ x e. B C )
Theorem	mptelixpg 6788*	Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.)
|- ( I e. V -> ( ( x e. I |-> J ) e. X_ x e. I K <-> A. x e. I J e. K ) )
Theorem	elixpsn 6789*	Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( A e. V -> ( F e. X_ x e. { A } B <-> E. y e. B F = { <. A , y >. } ) )
Theorem	ixpsnf1o 6790*	A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. A |-> ( { I } X. { x } ) )   =>    |- ( I e. V -> F : A -1-1-onto-> X_ y e. { I } A )
Theorem	mapsnf1o 6791*	A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- F = ( x e. A |-> ( { I } X. { x } ) )   =>    |- ( ( A e. V /\ I e. W ) -> F : A -1-1-onto-> ( A ^m { I } ) )
2.6.28  Equinumerosity
Syntax	cen 6792	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ~~
Syntax	cdom 6793	Extend class definition to include the dominance relation (curly less-than-or-equal)
class ~<_
Syntax	cfn 6794	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 6795*	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 6801. (Contributed by NM, 28-Mar-1998.)
|- ~~ = { <. x , y >. | E. f f : x -1-1-onto-> y }
Definition	df-dom 6796*	Define the dominance relation. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 6804 and domen 6805. (Contributed by NM, 28-Mar-1998.)
|- ~<_ = { <. x , y >. | E. f f : x -1-1-> y }
Definition	df-fin 6797*	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our " a e. Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 15468. (Contributed by NM, 22-Aug-2008.)
|- Fin = { x | E. y e. om x ~~ y }
Theorem	relen 6798	Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~~
Theorem	reldom 6799	Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
|- Rel ~<_
Theorem	encv 6800	If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.)
|- ( A ~~ B -> ( A e. _V /\ B e. _V ) )