P. 64 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6301-6400   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cofr 6301	Extend class notation to include mapping of a binary relation to a function relation.
class oR R
Definition	df-of 6302*	Define the function operation map. The definition is designed so that if R is a binary operation, then oF R is the analogous operation on functions which corresponds to applying R pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
Definition	df-ofr 6303*	Define the function relation map. The definition is designed so that if R is a binary relation, then oF R is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
Theorem	ofeqd 6304	Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.)
|- ( ph -> R = S )   =>    |- ( ph -> oF R = oF S )
Theorem	ofeq 6305	Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( R = S -> oF R = oF S )
Theorem	ofreq 6306	Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( R = S -> oR R = oR S )
Theorem	ofexg 6307	A function operation restricted to a set is a set. (Contributed by NM, 28-Jul-2014.)
|- ( A e. V -> ( oF R |` A ) e. _V )
Theorem	nfof 6308	Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oF R
Theorem	nfofr 6309	Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oR R
Theorem	offval 6310*	Value of an operation applied to two functions. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = C )   &    |- ( ( ph /\ x e. B ) -> ( G ` x ) = D )   =>    |- ( ph -> ( F oF R G ) = ( x e. S |-> ( C R D ) ) )
Theorem	ofrfval 6311*	Value of a relation applied to two functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = C )   &    |- ( ( ph /\ x e. B ) -> ( G ` x ) = D )   =>    |- ( ph -> ( F oR R G <-> A. x e. S C R D ) )
Theorem	ofvalg 6312	Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   &    |- ( ( ph /\ X e. B ) -> ( G ` X ) = D )   &    |- ( ( ph /\ X e. S ) -> ( C R D ) e. U )   =>    |- ( ( ph /\ X e. S ) -> ( ( F oF R G ) ` X ) = ( C R D ) )
Theorem	ofrval 6313	Exhibit a function relation at a point. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = S   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   &    |- ( ( ph /\ X e. B ) -> ( G ` X ) = D )   =>    |- ( ( ph /\ F oR R G /\ X e. S ) -> C R D )
Theorem	ofmresval 6314	Value of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
|- ( ph -> F e. A )   &    |- ( ph -> G e. B )   =>    |- ( ph -> ( F ( oF R |` ( A X. B ) ) G ) = ( F oF R G ) )
Theorem	off 6315*	The function operation produces a function. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : B --> T )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( F oF R G ) : C --> U )
Theorem	offeq 6316*	Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Jim Kingdon, 26-Nov-2023.)
|- ( ( ph /\ ( x e. S /\ y e. T ) ) -> ( x R y ) e. U )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : B --> T )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = C   &    |- ( ph -> H : C --> U )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = D )   &    |- ( ( ph /\ x e. B ) -> ( G ` x ) = E )   &    |- ( ( ph /\ x e. C ) -> ( D R E ) = ( H ` x ) )   =>    |- ( ph -> ( F oF R G ) = H )
Theorem	ofres 6317	Restrict the operands of a function operation to the same domain as that of the operation itself. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( F oF R G ) = ( ( F |` C ) oF R ( G |` C ) ) )
Theorem	offval2 6318*	The function operation expressed as a mapping. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> C e. X )   &    |- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ph -> G = ( x e. A |-> C ) )   =>    |- ( ph -> ( F oF R G ) = ( x e. A |-> ( B R C ) ) )
Theorem	ofrfval2 6319*	The function relation acting on maps. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> C e. X )   &    |- ( ph -> F = ( x e. A |-> B ) )   &    |- ( ph -> G = ( x e. A |-> C ) )   =>    |- ( ph -> ( F oR R G <-> A. x e. A B R C ) )
Theorem	suppssof1 6320*	Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- ( ph -> ( `' A " ( _V \ { Y } ) ) C_ L )   &    |- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )   &    |- ( ph -> A : D --> V )   &    |- ( ph -> B : D --> R )   &    |- ( ph -> D e. W )   =>    |- ( ph -> ( `' ( A oF O B ) " ( _V \ { Z } ) ) C_ L )
Theorem	ofco 6321	The composition of a function operation with another function. (Contributed by Mario Carneiro, 19-Dec-2014.)
|- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> H : D --> C )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. X )   &    |- ( A i^i B ) = C   =>    |- ( ph -> ( ( F oF R G ) o. H ) = ( ( F o. H ) oF R ( G o. H ) ) )
Theorem	offveqb 6322*	Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> H Fn A )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   &    |- ( ( ph /\ x e. A ) -> ( G ` x ) = C )   =>    |- ( ph -> ( H = ( F oF R G ) <-> A. x e. A ( H ` x ) = ( B R C ) ) )
Theorem	offveq 6323*	Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn A )   &    |- ( ph -> H Fn A )   &    |- ( ( ph /\ x e. A ) -> ( F ` x ) = B )   &    |- ( ( ph /\ x e. A ) -> ( G ` x ) = C )   &    |- ( ( ph /\ x e. A ) -> ( B R C ) = ( H ` x ) )   =>    |- ( ph -> ( F oF R G ) = H )
Theorem	ofc1g 6324	Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F Fn A )   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   &    |- ( ( ph /\ X e. A ) -> ( B R C ) e. U )   =>    |- ( ( ph /\ X e. A ) -> ( ( ( A X. { B } ) oF R F ) ` X ) = ( B R C ) )
Theorem	ofc2g 6325	Right operation by a constant. (Contributed by NM, 7-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F Fn A )   &    |- ( ( ph /\ X e. A ) -> ( F ` X ) = C )   &    |- ( ( ph /\ X e. A ) -> ( C R B ) e. U )   =>    |- ( ( ph /\ X e. A ) -> ( ( F oF R ( A X. { B } ) ) ` X ) = ( C R B ) )
Theorem	ofc12 6326	Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( ( A X. { B } ) oF R ( A X. { C } ) ) = ( A X. { ( B R C ) } ) )
Theorem	caofref 6327*	Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ( ph /\ x e. S ) -> x R x )   =>    |- ( ph -> F oR R F )
Theorem	caofinvl 6328*	Transfer a left inverse law to the function operation. (Contributed by NM, 22-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> N : S --> S )   &    |- ( ph -> G = ( v e. A |-> ( N ` ( F ` v ) ) ) )   &    |- ( ( ph /\ x e. S ) -> ( ( N ` x ) R x ) = B )   =>    |- ( ph -> ( G oF R F ) = ( A X. { B } ) )
Theorem	caofid0l 6329*	Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ x e. S ) -> ( B R x ) = x )   =>    |- ( ph -> ( ( A X. { B } ) oF R F ) = F )
Theorem	caofid0r 6330*	Transfer a right identity law to the function operation. (Contributed by NM, 21-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ x e. S ) -> ( x R B ) = x )   =>    |- ( ph -> ( F oF R ( A X. { B } ) ) = F )
Theorem	caofid1 6331*	Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ( ph /\ x e. S ) -> ( x R B ) = C )   =>    |- ( ph -> ( F oF R ( A X. { B } ) ) = ( A X. { C } ) )
Theorem	caofid2 6332*	Transfer a right absorption law to the function operation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ( ph /\ x e. S ) -> ( B R x ) = C )   =>    |- ( ph -> ( ( A X. { B } ) oF R F ) = ( A X. { C } ) )
Theorem	caofcom 6333*	Transfer a commutative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y ) = ( y R x ) )   =>    |- ( ph -> ( F oF R G ) = ( G oF R F ) )
Theorem	caofrss 6334*	Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y -> x T y ) )   =>    |- ( ph -> ( F oR R G -> F oR T G ) )
Theorem	caoftrn 6335*	Transfer a transitivity law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> S )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y /\ y T z ) -> x U z ) )   =>    |- ( ph -> ( ( F oR R G /\ G oR T H ) -> F oR U H ) )
Theorem	caofdig 6336*	Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> K )   &    |- ( ph -> G : A --> S )   &    |- ( ph -> H : A --> S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y ) e. V )   &    |- ( ( ph /\ ( x e. K /\ y e. S ) ) -> ( x T y ) e. W )   &    |- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x T ( y R z ) ) = ( ( x T y ) O ( x T z ) ) )   =>    |- ( ph -> ( F oF T ( G oF R H ) ) = ( ( F oF T G ) oF O ( F oF T H ) ) )
2.6.14  Functions (continued)
Theorem	resfunexgALT 6337	The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. This version has a shorter proof than resfunexg 5936 but requires ax-pow 4311 and ax-un 4578. (Contributed by NM, 7-Apr-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V )
Theorem	cofunexg 6338	Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007.)
|- ( ( Fun A /\ B e. C ) -> ( A o. B ) e. _V )
Theorem	cofunex2g 6339	Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007.)
|- ( ( A e. V /\ Fun `' B ) -> ( A o. B ) e. _V )
Theorem	fnexALT 6340	If the domain of a function is a set, the function is a set. Theorem 6.16(1) of [TakeutiZaring] p. 28. This theorem is derived using the Axiom of Replacement in the form of funimaexg 5465. This version of fnex 5937 uses ax-pow 4311 and ax-un 4578, whereas fnex 5937 does not. (Contributed by NM, 14-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( F Fn A /\ A e. B ) -> F e. _V )
Theorem	funexw 6341	Weak version of funex 5940 that holds without ax-coll 4246. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|- ( ( Fun F /\ dom F e. B /\ ran F e. C ) -> F e. _V )
Theorem	mptexw 6342*	Weak version of mptex 5943 that holds without ax-coll 4246. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.)
|- A e. _V   &    |- C e. _V   &    |- A. x e. A B e. C   =>    |- ( x e. A |-> B ) e. _V
Theorem	funrnex 6343	If the domain of a function exists, so does its range. Part of Theorem 4.15(v) of [Monk1] p. 46. This theorem is derived using the Axiom of Replacement in the form of funex 5940. (Contributed by NM, 11-Nov-1995.)
|- ( dom F e. B -> ( Fun F -> ran F e. _V ) )
Theorem	focdmex 6344	If the domain of an onto function exists, so does its codomain. (Contributed by NM, 23-Jul-2004.)
|- ( A e. C -> ( F : A -onto-> B -> B e. _V ) )
Theorem	f1dmex 6345	If the codomain of a one-to-one function exists, so does its domain. This can be thought of as a form of the Axiom of Replacement. (Contributed by NM, 4-Sep-2004.)
|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )
Theorem	abrexex 6346*	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in the class expression substituted for B, which can be thought of as B ( x ). This simple-looking theorem is actually quite powerful and appears to involve the Axiom of Replacement in an intrinsic way, as can be seen by tracing back through the path mptexg 5942, funex 5940, fnex 5937, resfunexg 5936, and funimaexg 5465. See also abrexex2 6353. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   =>    |- { y | E. x e. A y = B } e. _V
Theorem	abrexexg 6347*	Existence of a class abstraction of existentially restricted sets. x is normally a free-variable parameter in B. The antecedent assures us that A is a set. (Contributed by NM, 3-Nov-2003.)
|- ( A e. V -> { y | E. x e. A y = B } e. _V )
Theorem	iunexg 6348*	The existence of an indexed union. x is normally a free-variable parameter in B. (Contributed by NM, 23-Mar-2006.)
|- ( ( A e. V /\ A. x e. A B e. W ) -> U_ x e. A B e. _V )
Theorem	abrexex2g 6349*	Existence of an existentially restricted class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. V /\ A. x e. A { y | ph } e. W ) -> { y | E. x e. A ph } e. _V )
Theorem	opabex3d 6350*	Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.)
|- ( ph -> A e. _V )   &    |- ( ( ph /\ x e. A ) -> { y | ps } e. _V )   =>    |- ( ph -> { <. x , y >. | ( x e. A /\ ps ) } e. _V )
Theorem	opabex3 6351*	Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- A e. _V   &    |- ( x e. A -> { y | ph } e. _V )   =>    |- { <. x , y >. | ( x e. A /\ ph ) } e. _V
Theorem	iunex 6352*	The existence of an indexed union. x is normally a free-variable parameter in the class expression substituted for B, which can be read informally as B ( x ). (Contributed by NM, 13-Oct-2003.)
|- A e. _V   &    |- B e. _V   =>    |- U_ x e. A B e. _V
Theorem	abrexex2 6353*	Existence of an existentially restricted class abstraction. ph is normally has free-variable parameters x and y. See also abrexex 6346. (Contributed by NM, 12-Sep-2004.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x e. A ph } e. _V
Theorem	abexssex 6354*	Existence of a class abstraction with an existentially quantified expression. Both x and y can be free in ph. (Contributed by NM, 29-Jul-2006.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x ( x C_ A /\ ph ) } e. _V
Theorem	abexex 6355*	A condition where a class builder continues to exist after its wff is existentially quantified. (Contributed by NM, 4-Mar-2007.)
|- A e. _V   &    |- ( ph -> x e. A )   &    |- { y | ph } e. _V   =>    |- { y | E. x ph } e. _V
Theorem	elabreximd 6356*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- F/ x ph   &    |- F/ x ch   &    |- ( A = B -> ( ch <-> ps ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. C ) -> ps )   =>    |- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )
Theorem	elabreximdv 6357*	Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
|- ( A = B -> ( ch <-> ps ) )   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. C ) -> ps )   =>    |- ( ( ph /\ A e. { y | E. x e. C y = B } ) -> ch )
Theorem	abrexss 6358*	A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.)
|- F/_ x C   =>    |- ( A. x e. A B e. C -> { y | E. x e. A y = B } C_ C )
Theorem	funimass4f 6359	Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ x F   =>    |- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )
Theorem	oprabexd 6360*	Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ph -> A e. _V )   &    |- ( ph -> B e. _V )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> E* z ps )   &    |- ( ph -> F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ps ) } )   =>    |- ( ph -> F e. _V )
Theorem	oprabex 6361*	Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004.)
|- A e. _V   &    |- B e. _V   &    |- ( ( x e. A /\ y e. B ) -> E* z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) }   =>    |- F e. _V
Theorem	oprabex3 6362*	Existence of an operation class abstraction (special case). (Contributed by NM, 19-Oct-2004.)
|- H e. _V   &    |- F = { <. <. x , y >. , z >. | ( ( x e. ( H X. H ) /\ y e. ( H X. H ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = R ) ) }   =>    |- F e. _V
Theorem	oprabrexex2 6363*	Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.)
|- A e. _V   &    |- { <. <. x , y >. , z >. | ph } e. _V   =>    |- { <. <. x , y >. , z >. | E. w e. A ph } e. _V
Theorem	ab2rexex 6364*	Existence of a class abstraction of existentially restricted sets. Variables x and y are normally free-variable parameters in the class expression substituted for C, which can be thought of as C ( x , y ). See comments for abrexex 6346. (Contributed by NM, 20-Sep-2011.)
|- A e. _V   &    |- B e. _V   =>    |- { z | E. x e. A E. y e. B z = C } e. _V
Theorem	ab2rexex2 6365*	Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x, y, and z. Compare abrexex2 6353. (Contributed by NM, 20-Sep-2011.)
|- A e. _V   &    |- B e. _V   &    |- { z | ph } e. _V   =>    |- { z | E. x e. A E. y e. B ph } e. _V
Theorem	xpexgALT 6366	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4889 for a version that uses the Power Set axiom instead. (Contributed by Mario Carneiro, 20-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. V /\ B e. W ) -> ( A X. B ) e. _V )
Theorem	offval3 6367*	General value of ( F oF R G ) with no assumptions on functionality of F and G. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
Theorem	offres 6368	Pointwise combination commutes with restriction. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) |` D ) = ( ( F |` D ) oF R ( G |` D ) ) )
Theorem	ofmres 6369*	Equivalent expressions for a restriction of the function operation map. Unlike oF R which is a proper class, ( oF R |` ( A X. B ) ) can be a set by ofmresex 6370, allowing it to be used as a function or structure argument. By ofmresval 6314, the restricted operation map values are the same as the original values, allowing theorems for oF R to be reused. (Contributed by NM, 20-Oct-2014.)
|- ( oF R |` ( A X. B ) ) = ( f e. A , g e. B |-> ( f oF R g ) )
Theorem	ofmresex 6370	Existence of a restriction of the function operation map. (Contributed by NM, 20-Oct-2014.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( oF R |` ( A X. B ) ) e. _V )
Theorem	uchoice 6371*	Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7563 (with the key difference being the change of E. to E!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
|- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
2.6.15  First and second members of an ordered pair
Syntax	c1st 6372	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 6373	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 6374	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 6380 proves that it does this. For example, ( 1st ` <. 3 , 4 >.) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5269 and op1stb 4624). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 1st = ( x e. _V |-> U. dom { x } )
Definition	df-2nd 6375	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 6381 proves that it does this. For example, ( 2nd ` <. 3 , 4 >.) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5272 and op2ndb 5271). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 2nd = ( x e. _V |-> U. ran { x } )
Theorem	1stvalg 6376	The value of the function that extracts the first member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. _V -> ( 1st ` A ) = U. dom { A } )
Theorem	2ndvalg 6377	The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. _V -> ( 2nd ` A ) = U. ran { A } )
Theorem	1st0 6378	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 1st ` (/) ) = (/)
Theorem	2nd0 6379	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 2nd ` (/) ) = (/)
Theorem	op1st 6380	Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
|- A e. _V   &    |- B e. _V   =>    |- ( 1st ` <. A , B >. ) = A
Theorem	op2nd 6381	Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004.)
|- A e. _V   &    |- B e. _V   =>    |- ( 2nd ` <. A , B >. ) = B
Theorem	op1std 6382	Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( C = <. A , B >. -> ( 1st ` C ) = A )
Theorem	op2ndd 6383	Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- A e. _V   &    |- B e. _V   =>    |- ( C = <. A , B >. -> ( 2nd ` C ) = B )
Theorem	op1stg 6384	Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
|- ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )
Theorem	op2ndg 6385	Extract the second member of an ordered pair. (Contributed by NM, 19-Jul-2005.)
|- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )
Theorem	ot1stg 6386	Extract the first member of an ordered triple. (Due to infrequent usage, it isn't worthwhile at this point to define special extractors for triples, so we reuse the ordered pair extractors for ot1stg 6386, ot2ndg 6387, ot3rdgg 6388.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 1st ` ( 1st ` <. A , B , C >. ) ) = A )
Theorem	ot2ndg 6387	Extract the second member of an ordered triple. (See ot1stg 6386 comment.) (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 2-May-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` ( 1st ` <. A , B , C >. ) ) = B )
Theorem	ot3rdgg 6388	Extract the third member of an ordered triple. (See ot1stg 6386 comment.) (Contributed by NM, 3-Apr-2015.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( 2nd ` <. A , B , C >. ) = C )
Theorem	1stval2 6389	Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
|- ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )
Theorem	2ndval2 6390	Alternate value of the function that extracts the second member of an ordered pair. Definition 5.13 (ii) of [Monk1] p. 52. (Contributed by NM, 18-Aug-2006.)
|- ( A e. ( _V X. _V ) -> ( 2nd ` A ) = |^| |^| |^| `' { A } )
Theorem	fo1st 6391	The 1st function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- 1st : _V -onto-> _V
Theorem	fo2nd 6392	The 2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- 2nd : _V -onto-> _V
Theorem	f1stres 6393	Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A
Theorem	f2ndres 6394	Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B
Theorem	fo1stresm 6395*	Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|- ( E. y y e. B -> ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A )
Theorem	fo2ndresm 6396*	Onto mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Jim Kingdon, 24-Jan-2019.)
|- ( E. x x e. A -> ( 2nd |` ( A X. B ) ) : ( A X. B ) -onto-> B )
Theorem	1stcof 6397	Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007.)
|- ( F : A --> ( B X. C ) -> ( 1st o. F ) : A --> B )
Theorem	2ndcof 6398	Composition of the second member function with another function. (Contributed by FL, 15-Oct-2012.)
|- ( F : A --> ( B X. C ) -> ( 2nd o. F ) : A --> C )
Theorem	xp1st 6399	Location of the first element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. ( B X. C ) -> ( 1st ` A ) e. B )
Theorem	xp2nd 6400	Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( A e. ( B X. C ) -> ( 2nd ` A ) e. C )