P. 61 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6001-6100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	caov32d 6001*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( ( A F B ) F C ) = ( ( A F C ) F B ) )
Theorem	caov12d 6002*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( A F ( B F C ) ) = ( B F ( A F C ) ) )
Theorem	caov31d 6003*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( ( A F B ) F C ) = ( ( C F B ) F A ) )
Theorem	caov13d 6004*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ph -> ( A F ( B F C ) ) = ( C F ( B F A ) ) )
Theorem	caov4d 6005*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> D e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( B F D ) ) )
Theorem	caov411d 6006*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> D e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( C F B ) F ( A F D ) ) )
Theorem	caov42d 6007*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> D e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( D F B ) ) )
Theorem	caov32 6008*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( A F B ) F C ) = ( ( A F C ) F B )
Theorem	caov12 6009*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( A F ( B F C ) ) = ( B F ( A F C ) )
Theorem	caov31 6010*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( A F B ) F C ) = ( ( C F B ) F A )
Theorem	caov13 6011*	Rearrange arguments in a commutative, associative operation. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( A F ( B F C ) ) = ( C F ( B F A ) )
Theorem	caovdilemd 6012*	Lemma used by real number construction. (Contributed by Jim Kingdon, 16-Sep-2019.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) G z ) = ( ( x G z ) F ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) e. S )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ph -> D e. S )   &    |- ( ph -> H e. S )   =>    |- ( ph -> ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) ) )
Theorem	caovlem2d 6013*	Rearrangement of expression involving multiplication ( G) and addition ( F). (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) G z ) = ( ( x G z ) F ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) e. S )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ph -> D e. S )   &    |- ( ph -> H e. S )   &    |- ( ph -> R e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   =>    |- ( ph -> ( ( ( ( A G C ) F ( B G D ) ) G H ) F ( ( ( A G D ) F ( B G C ) ) G R ) ) = ( ( A G ( ( C G H ) F ( D G R ) ) ) F ( B G ( ( C G R ) F ( D G H ) ) ) ) )
Theorem	caovimo 6014*	Uniqueness of inverse element in commutative, associative operation with identity. The identity element is B. (Contributed by Jim Kingdon, 18-Sep-2019.)
|- B e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x F y ) = ( y F x ) )   &    |- ( ( x e. S /\ y e. S /\ z e. S ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( x e. S -> ( x F B ) = x )   =>    |- ( A e. S -> E* w ( w e. S /\ ( A F w ) = B ) )
Theorem	grprinvlem 6015*	Lemma for grprinvd 6016. (Contributed by NM, 9-Aug-2013.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   &    |- ( ( ph /\ ps ) -> X e. B )   &    |- ( ( ph /\ ps ) -> ( X .+ X ) = X )   =>    |- ( ( ph /\ ps ) -> X = O )
Theorem	grprinvd 6016*	Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   &    |- ( ( ph /\ ps ) -> X e. B )   &    |- ( ( ph /\ ps ) -> N e. B )   &    |- ( ( ph /\ ps ) -> ( N .+ X ) = O )   =>    |- ( ( ph /\ ps ) -> ( X .+ N ) = O )
Theorem	grpridd 6017*	Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )   &    |- ( ph -> O e. B )   &    |- ( ( ph /\ x e. B ) -> ( O .+ x ) = x )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )   &    |- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = O )   =>    |- ( ( ph /\ x e. B ) -> ( x .+ O ) = x )
2.6.12  Maps-to notation
Theorem	elmpocl 6018*	If a two-parameter class is inhabited, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )
Theorem	elmpocl1 6019*	If a two-parameter class is inhabited, the first argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( X e. ( S F T ) -> S e. A )
Theorem	elmpocl2 6020*	If a two-parameter class is inhabited, the second argument is in its nominal domain. (Contributed by FL, 15-Oct-2012.) (Revised by Stefan O'Rear, 7-Mar-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( X e. ( S F T ) -> T e. B )
Theorem	elovmpo 6021*	Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.)
|- D = ( a e. A , b e. B |-> C )   &    |- C e. _V   &    |- ( ( a = X /\ b = Y ) -> C = E )   =>    |- ( F e. ( X D Y ) <-> ( X e. A /\ Y e. B /\ F e. E ) )
Theorem	f1ocnvd 6022*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. W )   &    |- ( ( ph /\ y e. B ) -> D e. X )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )
Theorem	f1od 6023*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. W )   &    |- ( ( ph /\ y e. B ) -> D e. X )   &    |- ( ph -> ( ( x e. A /\ y = C ) <-> ( y e. B /\ x = D ) ) )   =>    |- ( ph -> F : A -1-1-onto-> B )
Theorem	f1ocnv2d 6024*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ y e. B ) -> D e. A )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )   =>    |- ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( y e. B |-> D ) ) )
Theorem	f1o2d 6025*	Describe an implicit one-to-one onto function. (Contributed by Mario Carneiro, 12-May-2014.)
|- F = ( x e. A |-> C )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( ( ph /\ y e. B ) -> D e. A )   &    |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( x = D <-> y = C ) )   =>    |- ( ph -> F : A -1-1-onto-> B )
Theorem	f1opw2 6026*	A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 6027 avoids the Axiom of Replacement. (Contributed by Mario Carneiro, 26-Jun-2015.)
|- ( ph -> F : A -1-1-onto-> B )   &    |- ( ph -> ( `' F " a ) e. _V )   &    |- ( ph -> ( F " b ) e. _V )   =>    |- ( ph -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )
Theorem	f1opw 6027*	A one-to-one mapping induces a one-to-one mapping on power sets. (Contributed by Stefan O'Rear, 18-Nov-2014.) (Revised by Mario Carneiro, 26-Jun-2015.)
|- ( F : A -1-1-onto-> B -> ( b e. ~P A |-> ( F " b ) ) : ~P A -1-1-onto-> ~P B )
Theorem	suppssfv 6028*	Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- ( ph -> ( `' ( x e. D |-> A ) " ( _V \ { Y } ) ) C_ L )   &    |- ( ph -> ( F ` Y ) = Z )   &    |- ( ( ph /\ x e. D ) -> A e. V )   =>    |- ( ph -> ( `' ( x e. D |-> ( F ` A ) ) " ( _V \ { Z } ) ) C_ L )
Theorem	suppssov1 6029*	Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- ( ph -> ( `' ( x e. D |-> A ) " ( _V \ { Y } ) ) C_ L )   &    |- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )   &    |- ( ( ph /\ x e. D ) -> A e. V )   &    |- ( ( ph /\ x e. D ) -> B e. R )   =>    |- ( ph -> ( `' ( x e. D |-> ( A O B ) ) " ( _V \ { Z } ) ) C_ L )
2.6.13  Function operation
Syntax	cof 6030	Extend class notation to include mapping of an operation to a function operation.
class oF R
Syntax	cofr 6031	Extend class notation to include mapping of a binary relation to a function relation.
class oR R
Definition	df-of 6032*	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 6033*	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	ofeq 6034	Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( R = S -> oF R = oF S )
Theorem	ofreq 6035	Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( R = S -> oR R = oR S )
Theorem	ofexg 6036	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 6037	Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oF R
Theorem	nfofr 6038	Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oR R
Theorem	offval 6039*	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 6040*	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 6041	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 6042	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 6043	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 6044*	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 6045*	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 6046	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 6047*	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 6048*	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 6049*	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 6050	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 6051*	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	ofc12 6052	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 6053*	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 6054*	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	caofcom 6055*	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 6056*	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 6057*	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 ) )
2.6.14  Functions (continued)
Theorem	resfunexgALT 6058	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 5688 but requires ax-pow 4135 and ax-un 4393. (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 6059	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 6060	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 6061	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 5254. This version of fnex 5689 uses ax-pow 4135 and ax-un 4393, whereas fnex 5689 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	funrnex 6062	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 5690. (Contributed by NM, 11-Nov-1995.)
|- ( dom F e. B -> ( Fun F -> ran F e. _V ) )
Theorem	fornex 6063	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 6064	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 6065*	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 5692, funex 5690, fnex 5689, resfunexg 5688, and funimaexg 5254. See also abrexex2 6072. (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 6066*	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 6067*	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 6068*	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 6069*	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 6070*	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 6071*	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 6072*	Existence of an existentially restricted class abstraction. ph is normally has free-variable parameters x and y. See also abrexex 6065. (Contributed by NM, 12-Sep-2004.)
|- A e. _V   &    |- { y | ph } e. _V   =>    |- { y | E. x e. A ph } e. _V
Theorem	abexssex 6073*	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 6074*	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	oprabexd 6075*	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 6076*	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 6077*	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 6078*	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 6079*	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 6065. (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 6080*	Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x, y, and z. Compare abrexex2 6072. (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 6081	The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. This version is proven using Replacement; see xpexg 4700 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 6082*	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 6083	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 6084*	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 6085, allowing it to be used as a function or structure argument. By ofmresval 6043, 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 6085	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 )
2.6.15  First and second members of an ordered pair
Syntax	c1st 6086	Extend the definition of a class to include the first member an ordered pair function.
class 1st
Syntax	c2nd 6087	Extend the definition of a class to include the second member an ordered pair function.
class 2nd
Definition	df-1st 6088	Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 6094 proves that it does this. For example, ( 1st ` <. 3 , 4 >.) = 3 . Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 5067 and op1stb 4438). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 1st = ( x e. _V |-> U. dom { x } )
Definition	df-2nd 6089	Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd 6095 proves that it does this. For example, ( 2nd ` <. 3 , 4 >.) = 4 . Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 5070 and op2ndb 5069). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004.)
|- 2nd = ( x e. _V |-> U. ran { x } )
Theorem	1stvalg 6090	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 6091	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 6092	The value of the first-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 1st ` (/) ) = (/)
Theorem	2nd0 6093	The value of the second-member function at the empty set. (Contributed by NM, 23-Apr-2007.)
|- ( 2nd ` (/) ) = (/)
Theorem	op1st 6094	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 6095	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 6096	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 6097	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 6098	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 6099	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 6100	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 6100, ot2ndg 6101, ot3rdgg 6102.) (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 )