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	th3qlem1 6901*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. (Contributed by NM, 3-Aug-1995.) (Revised by Mario Carneiro, 9-Jul-2014.)
|- .~ Er S   &    |- ( ( ( y e. S /\ w e. S ) /\ ( z e. S /\ v e. S ) ) -> ( ( y .~ w /\ z .~ v ) -> ( y .+ z ) .~ ( w .+ v ) ) )   =>    |- ( ( A e. ( S /. .~ ) /\ B e. ( S /. .~ ) ) -> E* x E. y E. z ( ( A = [ y ] .~ /\ B = [ z ] .~ ) /\ x = [ ( y .+ z ) ] .~ ) )
Theorem	th3qlem2 6902*	Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   =>    |- ( ( A e. ( ( S X. S ) /. .~ ) /\ B e. ( ( S X. S ) /. .~ ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] .~ /\ B = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) )
Theorem	th3qcor 6903*	Corollary of Theorem 3Q of [Enderton] p. 60. (Contributed by NM, 12-Nov-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   &    |- G = { <. <. x , y >. , z >. | ( ( x e. ( ( S X. S ) /. .~ ) /\ y e. ( ( S X. S ) /. .~ ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] .~ /\ y = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) ) }   =>    |- Fun G
Theorem	th3q 6904*	Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- ( ( ( ( w e. S /\ v e. S ) /\ ( u e. S /\ t e. S ) ) /\ ( ( s e. S /\ f e. S ) /\ ( g e. S /\ h e. S ) ) ) -> ( ( <. w , v >. .~ <. u , t >. /\ <. s , f >. .~ <. g , h >. ) -> ( <. w , v >. .+ <. s , f >. ) .~ ( <. u , t >. .+ <. g , h >. ) ) )   &    |- G = { <. <. x , y >. , z >. | ( ( x e. ( ( S X. S ) /. .~ ) /\ y e. ( ( S X. S ) /. .~ ) ) /\ E. w E. v E. u E. t ( ( x = [ <. w , v >. ] .~ /\ y = [ <. u , t >. ] .~ ) /\ z = [ ( <. w , v >. .+ <. u , t >. ) ] .~ ) ) }   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ G [ <. C , D >. ] .~ ) = [ ( <. A , B >. .+ <. C , D >. ) ] .~ )
Theorem	oviec 6905*	Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. See iset.mm for additional comments describing the hypotheses. (Unnecessary distinct variable restrictions were removed by David Abernethy, 4-Jun-2013.) (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 4-Jun-2013.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> H e. ( S X. S ) )   &    |- ( ( ( a e. S /\ b e. S ) /\ ( g e. S /\ h e. S ) ) -> K e. ( S X. S ) )   &    |- ( ( ( c e. S /\ d e. S ) /\ ( t e. S /\ s e. S ) ) -> L e. ( S X. S ) )   &    |- .~ e. _V   &    |- .~ Er ( S X. S )   &    |- .~ = { <. x , y >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ph ) ) }   &    |- ( ( ( z = a /\ w = b ) /\ ( v = c /\ u = d ) ) -> ( ph <-> ps ) )   &    |- ( ( ( z = g /\ w = h ) /\ ( v = t /\ u = s ) ) -> ( ph <-> ch ) )   &    |- .+ = { <. <. x , y >. , z >. | ( ( x e. ( S X. S ) /\ y e. ( S X. S ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = J ) ) }   &    |- ( ( ( w = a /\ v = b ) /\ ( u = g /\ f = h ) ) -> J = K )   &    |- ( ( ( w = c /\ v = d ) /\ ( u = t /\ f = s ) ) -> J = L )   &    |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> J = H )   &    |- .+^ = { <. <. x , y >. , z >. | ( ( x e. Q /\ y e. Q ) /\ E. a E. b E. c E. d ( ( x = [ <. a , b >. ] .~ /\ y = [ <. c , d >. ] .~ ) /\ z = [ ( <. a , b >. .+ <. c , d >. ) ] .~ ) ) }   &    |- Q = ( ( S X. S ) /. .~ )   &    |- ( ( ( ( a e. S /\ b e. S ) /\ ( c e. S /\ d e. S ) ) /\ ( ( g e. S /\ h e. S ) /\ ( t e. S /\ s e. S ) ) ) -> ( ( ps /\ ch ) -> K .~ L ) )   =>    |- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( [ <. A , B >. ] .~ .+^ [ <. C , D >. ] .~ ) = [ H ] .~ )
Theorem	ecovcom 6906*	Lemma used to transfer a commutative law via an equivalence relation. Most uses will want ecovicom 6907 instead. (Contributed by NM, 29-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- C = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- D = H   &    |- G = J   =>    |- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )
Theorem	ecovicom 6907*	Lemma used to transfer a commutative law via an equivalence relation. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- C = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> D = H )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> G = J )   =>    |- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )
Theorem	ecovass 6908*	Lemma used to transfer an associative law via an equivalence relation. In most cases ecoviass 6909 will be more useful. (Contributed by NM, 31-Aug-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )   &    |- ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )   &    |- J = L   &    |- K = M   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )
Theorem	ecoviass 6909*	Lemma used to transfer an associative law via an equivalence relation. (Contributed by Jim Kingdon, 16-Sep-2019.)
|- D = ( ( S X. S ) /. .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )   &    |- ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )   &    |- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> J = L )   &    |- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> K = M )   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )
Theorem	ecovdi 6910*	Lemma used to transfer a distributive law via an equivalence relation. Most likely ecovidi 6911 will be more helpful. (Contributed by NM, 2-Sep-1995.) (Revised by David Abernethy, 4-Jun-2013.)
|- 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 ) )   &    |- H = K   &    |- J = L   =>    |- ( ( A e. D /\ B e. D /\ C e. D ) -> ( A .x. ( B .+ C ) ) = ( ( A .x. B ) .+ ( A .x. C ) ) )
Theorem	ecovidi 6911*	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.27  The mapping operation
Syntax	cmap 6912	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 6913	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 6914*	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 6924). 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 6915*	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 6923). 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 6914) . See mapsspm 6953 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 6916*	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 6917*	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 6918*	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 6919	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 6920	Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ^pm Fn ( _V X. _V )
Theorem	reldmmap 6921	Set exponentiation is a well-behaved binary operator. (Contributed by Stefan O'Rear, 27-Feb-2015.)
|- Rel dom ^m
Theorem	mapvalg 6922*	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 6923*	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 6924*	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 6925	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 6926	Deduction form of elmapg 6925. (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 6927	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 6928	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 6929	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 6930	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 6931	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 6932	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 6933	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 6934	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	mapfset 6935*	If B is a set, the value of the set exponentiation ( B ^m A ) is the class of all functions from A to B. Generalisation of mapvalg 6922 to arbitrary domains. Note that the class { f | f : A --> B } can only contain set-functions, as opposed to arbitrary class-functions. When A is a proper class, there can be no set-functions on it, so the above class is empty (see also fsetdmprc0 6940), hence a set. In this case, both sides of the equality in this theorem are the empty set. (Contributed by AV, 8-Aug-2024.)
|- ( B e. V -> { f | f : A --> B } = ( B ^m A ) )
Theorem	mapssfsetg 6936*	The value of the set exponentiation ( B ^m A ) is a subset of the class of functions from A to B. (Contributed by AV, 10-Aug-2024.)
|- ( B e. V -> ( B ^m A ) C_ { f | f : A --> B } )
Theorem	mapfoss 6937*	The value of the set exponentiation ( B ^m A ) is a superset of the set of all functions from A onto B. (Contributed by AV, 7-Aug-2024.)
|- { f | f : A -onto-> B } C_ ( B ^m A )
Theorem	fsetsspwxp 6938*	The class of all functions from A into B is a subclass of the power class of the cartesion product of A and B. (Contributed by AV, 13-Sep-2024.)
|- { f | f : A --> B } C_ ~P ( A X. B )
Theorem	fset0 6939	The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.)
|- { f | f : (/) --> B } = { (/) }
Theorem	fsetdmprc0 6940*	The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.)
|- ( A e/ _V -> { f | f Fn A } = (/) )
Theorem	f1setexg 6941*	The set of injections between two sets exists. (Contributed by AV, 14-Aug-2024.)
|- ( ( A e. V /\ B e. W ) -> { f | f : A -1-1-> B } e. _V )
Theorem	elmapfn 6942	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 6943	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 6944	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 6945	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 6946	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 6947	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 6948	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 6949*	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 6950	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 6951	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 6952	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 6953	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 6954	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 6955	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 6956*	Special case of fvmpt 5776 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 6957	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 6958	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 6959	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	mapsnd 6960*	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.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )
Theorem	map0 6961	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 6962*	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 6963	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 6964*	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 6965*	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 6966	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 6967*	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 6968*	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 6969*	Explicit bijection in the reverse of mapsnf1o2 6968. (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.28  Infinite Cartesian products
Syntax	cixp 6970	Extend class notation to include infinite Cartesian products.
class X_ x e. A B
Definition	df-ixp 6971*	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 6972*	Eliminate the expression { x | x e. A } in df-ixp 6971, 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 6973*	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 6974*	Membership in an infinite Cartesian product. See df-ixp 6971 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 6975*	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 6976*	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 6977*	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 6978*	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 6979*	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 6980*	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 6981*	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 6982*	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 6983	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 6984	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 6985*	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 6986*	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 6987*	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 6988*	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 6989*	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 6990	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 6991*	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 6992*	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 6993*	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 6994*	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 6995*	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 6996*	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 6997*	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 6998	An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.)
|- X_ x e. (/) A = { (/) }
Theorem	ixpssmap2g 6999*	An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 7000 avoids ax-coll 4241. (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 7000*	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 ) )