P. 62 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6101-6200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	caovcomg 6101*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S ) ) -> ( A F B ) = ( B F A ) )
Theorem	caovcomd 6102*	Convert an operation commutative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   =>    |- ( ph -> ( A F B ) = ( B F A ) )
Theorem	caovcom 6103*	Convert an operation commutative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 1-Jun-2013.)
|- A e. _V   &    |- B e. _V   &    |- ( x F y ) = ( y F x )   =>    |- ( A F B ) = ( B F A )
Theorem	caovassg 6104*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 1-Jun-2013.) (Revised by Mario Carneiro, 26-May-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	caovassd 6105*	Convert an operation associative law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x F y ) F z ) = ( x F ( y F z ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	caovass 6106*	Convert an operation associative law to class notation. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( A F B ) F C ) = ( A F ( B F C ) )
Theorem	caovcang 6107*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )   =>    |- ( ( ph /\ ( A e. T /\ B e. S /\ C e. S ) ) -> ( ( A F B ) = ( A F C ) <-> B = C ) )
Theorem	caovcand 6108*	Convert an operation cancellation law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( ( A F B ) = ( A F C ) <-> B = C ) )
Theorem	caovcanrd 6109*	Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )   &    |- ( ph -> A e. T )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ph -> A e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )   =>    |- ( ph -> ( ( B F A ) = ( C F A ) <-> B = C ) )
Theorem	caovcan 6110*	Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995.)
|- C e. _V   &    |- ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F z ) -> y = z ) )   =>    |- ( ( A e. S /\ B e. S ) -> ( ( A F B ) = ( A F C ) -> B = C ) )
Theorem	caovordig 6111*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y -> ( z F x ) R ( z F y ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( A R B -> ( C F A ) R ( C F B ) ) )
Theorem	caovordid 6112*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 31-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y -> ( z F x ) R ( z F y ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( A R B -> ( C F A ) R ( C F B ) ) )
Theorem	caovordg 6113*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	caovordd 6114*	Convert an operation ordering law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	caovord2d 6115*	Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- ( 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 -> ( A R B <-> ( A F C ) R ( B F C ) ) )
Theorem	caovord3d 6116*	Ordering law. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- ( 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 -> D e. S )   =>    |- ( ph -> ( ( A F B ) = ( C F D ) -> ( A R C <-> D R B ) ) )
Theorem	caovord 6117*	Convert an operation ordering law to class notation. (Contributed by NM, 19-Feb-1996.)
|- A e. _V   &    |- B e. _V   &    |- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )   =>    |- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	caovord2 6118*	Operation ordering law with commuted arguments. (Contributed by NM, 27-Feb-1996.)
|- A e. _V   &    |- B e. _V   &    |- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   =>    |- ( C e. S -> ( A R B <-> ( A F C ) R ( B F C ) ) )
Theorem	caovord3 6119*	Ordering law. (Contributed by NM, 29-Feb-1996.)
|- A e. _V   &    |- B e. _V   &    |- ( z e. S -> ( x R y <-> ( z F x ) R ( z F y ) ) )   &    |- C e. _V   &    |- ( x F y ) = ( y F x )   &    |- D e. _V   =>    |- ( ( ( B e. S /\ C e. S ) /\ ( A F B ) = ( C F D ) ) -> ( A R C <-> D R B ) )
Theorem	caovdig 6120*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 26-Jul-2014.)
|- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) )   =>    |- ( ( ph /\ ( A e. K /\ B e. S /\ C e. S ) ) -> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) )
Theorem	caovdid 6121*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) H ( x G z ) ) )   &    |- ( ph -> A e. K )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   =>    |- ( ph -> ( A G ( B F C ) ) = ( ( A G B ) H ( A G C ) ) )
Theorem	caovdir2d 6122*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) e. S )   &    |- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x G y ) = ( y G x ) )   =>    |- ( ph -> ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) ) )
Theorem	caovdirg 6123*	Convert an operation reverse distributive law to class notation. (Contributed by Mario Carneiro, 19-Oct-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x F y ) G z ) = ( ( x G z ) H ( y G z ) ) )   =>    |- ( ( ph /\ ( A e. S /\ B e. S /\ C e. K ) ) -> ( ( A F B ) G C ) = ( ( A G C ) H ( B G C ) ) )
Theorem	caovdird 6124*	Convert an operation distributive law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x F y ) G z ) = ( ( x G z ) H ( y G z ) ) )   &    |- ( ph -> A e. S )   &    |- ( ph -> B e. S )   &    |- ( ph -> C e. K )   =>    |- ( ph -> ( ( A F B ) G C ) = ( ( A G C ) H ( B G C ) ) )
Theorem	caovdi 6125*	Convert an operation distributive law to class notation. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 28-Jun-2013.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) )   =>    |- ( A G ( B F C ) ) = ( ( A G B ) F ( A G C ) )
Theorem	caov32d 6126*	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 6127*	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 6128*	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 6129*	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 6130*	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 6131*	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 6132*	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 6133*	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 6134*	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 6135*	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 6136*	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 6137*	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 6138*	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 6139*	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 ) )
2.6.12  Maps-to notation
Theorem	elmpocl 6140*	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 6141*	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 6142*	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	elovmpod 6143*	Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6144 in deduction form. (Revised by AV, 20-Apr-2025.)
|- O = ( a e. A , b e. B |-> C )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   &    |- ( ph -> D e. V )   &    |- ( ( a = X /\ b = Y ) -> C = D )   =>    |- ( ph -> ( E e. ( X O Y ) <-> E e. D ) )
Theorem	elovmpo 6144*	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	elovmporab 6145*	Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- O = ( x e. _V , y e. _V |-> { z e. M | ph } )   &    |- ( ( X e. _V /\ Y e. _V ) -> M e. _V )   =>    |- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. M ) )
Theorem	elovmporab1w 6146*	Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by GG, 26-Jan-2024.)
|- O = ( x e. _V , y e. _V |-> { z e. [_ x / m ]_ M | ph } )   &    |- ( ( X e. _V /\ Y e. _V ) -> [_ X / m ]_ M e. _V )   =>    |- ( Z e. ( X O Y ) -> ( X e. _V /\ Y e. _V /\ Z e. [_ X / m ]_ M ) )
Theorem	f1ocnvd 6147*	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 6148*	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 6149*	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 6150*	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 6151*	A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 6152 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 6152*	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 6153*	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 6154*	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 6155	Extend class notation to include mapping of an operation to a function operation.
class oF R
Syntax	cofr 6156	Extend class notation to include mapping of a binary relation to a function relation.
class oR R
Definition	df-of 6157*	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 6158*	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 6159	Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.)
|- ( ph -> R = S )   =>    |- ( ph -> oF R = oF S )
Theorem	ofeq 6160	Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( R = S -> oF R = oF S )
Theorem	ofreq 6161	Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( R = S -> oR R = oR S )
Theorem	ofexg 6162	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 6163	Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oF R
Theorem	nfofr 6164	Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- F/_ x R   =>    |- F/_ x oR R
Theorem	offval 6165*	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 6166*	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 6167	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 6168	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 6169	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 6170*	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 6171*	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 6172	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 6173*	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 6174*	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 6175*	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 6176	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 6177*	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 6178*	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 6179	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 6180	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 6181	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 6182*	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 6183*	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 6184*	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 6185*	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 6186*	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 6187*	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 6188*	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 6189*	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 6190*	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 6191*	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 6192	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 5804 but requires ax-pow 4217 and ax-un 4479. (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 6193	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 6194	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 6195	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 5357. This version of fnex 5805 uses ax-pow 4217 and ax-un 4479, whereas fnex 5805 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 6196	Weak version of funex 5806 that holds without ax-coll 4158. 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 6197*	Weak version of mptex 5809 that holds without ax-coll 4158. 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 6198	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 5806. (Contributed by NM, 11-Nov-1995.)
|- ( dom F e. B -> ( Fun F -> ran F e. _V ) )
Theorem	focdmex 6199	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 6200	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 )