P. 60 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 5901-6000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ov 5901*	The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- C e. _V   &    |- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( z = C -> ( ch <-> th ) )   &    |- ( ( x e. R /\ y e. S ) -> E! z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( A e. R /\ B e. S ) -> ( ( A F B ) = C <-> th ) )
Theorem	ovigg 5902*	The value of an operation class abstraction. Compare ovig 5903. The condition ( x e. R /\ y e. S ) is been removed. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )   &    |- E* z ph   &    |- F = { <. <. x , y >. , z >. | ph }   =>    |- ( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) )
Theorem	ovig 5903*	The value of an operation class abstraction (weak version). (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 14-Sep-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )   &    |- ( ( x e. R /\ y e. S ) -> E* z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( A e. R /\ B e. S /\ C e. D ) -> ( ps -> ( A F B ) = C ) )
Theorem	ovmpt4g 5904*	Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5542.) (Contributed by NM, 21-Feb-2004.) (Revised by Mario Carneiro, 1-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( x e. A /\ y e. B /\ C e. V ) -> ( x F y ) = C )
Theorem	ovmpt2s 5905*	Value of a function given by the "maps to" notation, expressed using explicit substitution. (Contributed by Mario Carneiro, 30-Apr-2015.)
|- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ [_ A / x ]_ [_ B / y ]_ R e. V ) -> ( A F B ) = [_ A / x ]_ [_ B / y ]_ R )
Theorem	ov2gf 5906*	The value of an operation class abstraction. A version of ovmpt2g 5916 using bound-variable hypotheses. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 19-Dec-2013.)
|- F/_ x A   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ x G   &    |- F/_ y S   &    |- ( x = A -> R = G )   &    |- ( y = B -> G = S )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpt2dxf 5907*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ x = A ) -> D = L )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. L )   &    |- ( ph -> S e. X )   &    |- F/ x ph   &    |- F/ y ph   &    |- F/_ y A   &    |- F/_ x B   &    |- F/_ x S   &    |- F/_ y S   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2dx 5908*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ( ph /\ x = A ) -> D = L )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. L )   &    |- ( ph -> S e. X )   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2d 5909*	Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
|- ( ph -> F = ( x e. C , y e. D |-> R ) )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. D )   &    |- ( ph -> S e. X )   =>    |- ( ph -> ( A F B ) = S )
Theorem	ovmpt2x 5910*	The value of an operation class abstraction. Variant of ovmpt2ga 5911 which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 20-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- ( x = A -> D = L )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. L /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpt2ga 5911*	Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpt2a 5912*	Value of an operation given by a maps-to rule. (Contributed by NM, 19-Dec-2013.)
|- ( ( x = A /\ y = B ) -> R = S )   &    |- F = ( x e. C , y e. D |-> R )   &    |- S e. _V   =>    |- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )
Theorem	ovmpt2df 5913*	Alternate deduction version of ovmpt2 5917, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. C )   &    |- ( ( ph /\ x = A ) -> B e. D )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = R -> ps ) )   &    |- F/_ x F   &    |- F/ x ps   &    |- F/_ y F   &    |- F/ y ps   =>    |- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )
Theorem	ovmpt2dv 5914*	Alternate deduction version of ovmpt2 5917, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. C )   &    |- ( ( ph /\ x = A ) -> B e. D )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( A F B ) = R -> ps ) )   =>    |- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ps ) )
Theorem	ovmpt2dv2 5915*	Alternate deduction version of ovmpt2 5917, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> A e. C )   &    |- ( ( ph /\ x = A ) -> B e. D )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R e. V )   &    |- ( ( ph /\ ( x = A /\ y = B ) ) -> R = S )   =>    |- ( ph -> ( F = ( x e. C , y e. D |-> R ) -> ( A F B ) = S ) )
Theorem	ovmpt2g 5916*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 14-Sep-1999.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( x = A -> R = G )   &    |- ( y = B -> G = S )   &    |- F = ( x e. C , y e. D |-> R )   =>    |- ( ( A e. C /\ B e. D /\ S e. H ) -> ( A F B ) = S )
Theorem	ovmpt2 5917*	Value of an operation given by a maps-to rule. Special case. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
|- ( x = A -> R = G )   &    |- ( y = B -> G = S )   &    |- F = ( x e. C , y e. D |-> R )   &    |- S e. _V   =>    |- ( ( A e. C /\ B e. D ) -> ( A F B ) = S )
Theorem	ov3 5918*	The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
|- S e. _V   &    |- ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> R = S )   &    |- 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 ) ) }   =>    |- ( ( ( A e. H /\ B e. H ) /\ ( C e. H /\ D e. H ) ) -> ( <. A , B >. F <. C , D >. ) = S )
Theorem	ov6g 5919*	The value of an operation class abstraction. Special case. (Contributed by NM, 13-Nov-2006.)
|- ( <. x , y >. = <. A , B >. -> R = S )   &    |- F = { <. <. x , y >. , z >. | ( <. x , y >. e. C /\ z = R ) }   =>    |- ( ( ( A e. G /\ B e. H /\ <. A , B >. e. C ) /\ S e. J ) -> ( A F B ) = S )
Theorem	ovg 5920*	The value of an operation class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)
|- ( x = A -> ( ph <-> ps ) )   &    |- ( y = B -> ( ps <-> ch ) )   &    |- ( z = C -> ( ch <-> th ) )   &    |- ( ( ta /\ ( x e. R /\ y e. S ) ) -> E! z ph )   &    |- F = { <. <. x , y >. , z >. | ( ( x e. R /\ y e. S ) /\ ph ) }   =>    |- ( ( ta /\ ( A e. R /\ B e. S /\ C e. D ) ) -> ( ( A F B ) = C <-> th ) )
Theorem	ovres 5921	The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
|- ( ( A e. C /\ B e. D ) -> ( A ( F |` ( C X. D ) ) B ) = ( A F B ) )
Theorem	ovresd 5922	Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( A ( D |` ( X X. X ) ) B ) = ( A D B ) )
Theorem	oprssov 5923	The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007.)
|- ( ( ( Fun F /\ G Fn ( C X. D ) /\ G C_ F ) /\ ( A e. C /\ B e. D ) ) -> ( A F B ) = ( A G B ) )
Theorem	fovrn 5924	An operation's value belongs to its codomain. (Contributed by NM, 27-Aug-2006.)
|- ( ( F : ( R X. S ) --> C /\ A e. R /\ B e. S ) -> ( A F B ) e. C )
Theorem	fovrnda 5925	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> F : ( R X. S ) --> C )   =>    |- ( ( ph /\ ( A e. R /\ B e. S ) ) -> ( A F B ) e. C )
Theorem	fovrnd 5926	An operation's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
|- ( ph -> F : ( R X. S ) --> C )   &    |- ( ph -> A e. R )   &    |- ( ph -> B e. S )   =>    |- ( ph -> ( A F B ) e. C )
Theorem	fnrnov 5927*	The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006.)
|- ( F Fn ( A X. B ) -> ran F = { z | E. x e. A E. y e. B z = ( x F y ) } )
Theorem	foov 5928*	An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006.)
|- ( F : ( A X. B ) -onto-> C <-> ( F : ( A X. B ) --> C /\ A. z e. C E. x e. A E. y e. B z = ( x F y ) ) )
Theorem	fnovrn 5929	An operation's value belongs to its range. (Contributed by NM, 10-Feb-2007.)
|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( C F D ) e. ran F )
Theorem	ovelrn 5930*	A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 30-Jan-2014.)
|- ( F Fn ( A X. B ) -> ( C e. ran F <-> E. x e. A E. y e. B C = ( x F y ) ) )
Theorem	funimassov 5931*	Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- ( ( Fun F /\ ( A X. B ) C_ dom F ) -> ( ( F " ( A X. B ) ) C_ C <-> A. x e. A A. y e. B ( x F y ) e. C ) )
Theorem	ovelimab 5932*	Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013.) (Revised by Mario Carneiro, 29-Jan-2014.)
|- ( ( F Fn A /\ ( B X. C ) C_ A ) -> ( D e. ( F " ( B X. C ) ) <-> E. x e. B E. y e. C D = ( x F y ) ) )
Theorem	ovconst2 5933	The value of a constant operation. (Contributed by NM, 5-Nov-2006.)
|- C e. _V   =>    |- ( ( R e. A /\ S e. B ) -> ( R ( ( A X. B ) X. { C } ) S ) = C )
Theorem	ab2rexex 5934*	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 5697. (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 5935*	Existence of an existentially restricted class abstraction. ph is normally has free-variable parameters x, y, and z. Compare abrexex2 5714. (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	oprssdm 5936*	Domain of closure of an operation. (Contributed by NM, 24-Aug-1995.)
|- -. (/) e. S   &    |- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )   =>    |- ( S X. S ) C_ dom F
Theorem	ndmovg 5937	The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008.)
|- ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> ( A F B ) = (/) )
Theorem	ndmov 5938	The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.)
|- dom F = ( S X. S )   =>    |- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = (/) )
Theorem	ndmovcl 5939	The closure of an operation outside its domain, when the domain includes the empty set. This technical lemma can make the operation more convenient to work in some cases. It is is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by NM, 24-Sep-2004.)
|- dom F = ( S X. S )   &    |- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )   &    |- (/) e. S   =>    |- ( A F B ) e. S
Theorem	ndmovrcl 5940	Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996.)
|- dom F = ( S X. S )   &    |- -. (/) e. S   =>    |- ( ( A F B ) e. S -> ( A e. S /\ B e. S ) )
Theorem	ndmovcom 5941	Any operation is commutative outside its domain. (Contributed by NM, 24-Aug-1995.)
|- dom F = ( S X. S )   =>    |- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = ( B F A ) )
Theorem	ndmovass 5942	Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
|- dom F = ( S X. S )   &    |- -. (/) e. S   =>    |- ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	ndmovdistr 5943	Any operation is distributive outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995.)
|- dom F = ( S X. S )   &    |- -. (/) e. S   &    |- dom G = ( S X. S )   =>    |- ( -. ( A e. S /\ B e. S /\ C e. S ) -> ( A G ( B F C ) ) = ( ( A G B ) F ( A G C ) ) )
Theorem	ndmovord 5944	Elimination of redundant antecedents in an ordering law. (Contributed by NM, 7-Mar-1996.)
|- dom F = ( S X. S )   &    |- R C_ ( S X. S )   &    |- -. (/) e. S   &    |- ( ( A e. S /\ B e. S /\ C e. S ) -> ( A R B <-> ( C F A ) R ( C F B ) ) )   =>    |- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )
Theorem	ndmovordi 5945	Elimination of redundant antecedent in an ordering law. (Contributed by NM, 25-Jun-1998.)
|- dom F = ( S X. S )   &    |- R C_ ( S X. S )   &    |- -. (/) e. S   &    |- ( C e. S -> ( A R B <-> ( C F A ) R ( C F B ) ) )   =>    |- ( ( C F A ) R ( C F B ) -> A R B )
Theorem	caovclg 5946*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
|- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E )   =>    |- ( ( ph /\ ( A e. C /\ B e. D ) ) -> ( A F B ) e. E )
Theorem	caovcld 5947*	Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014.)
|- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E )   &    |- ( ph -> A e. C )   &    |- ( ph -> B e. D )   =>    |- ( ph -> ( A F B ) e. E )
Theorem	caovcl 5948*	Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995.) (Revised by Mario Carneiro, 26-May-2014.)
|- ( ( x e. S /\ y e. S ) -> ( x F y ) e. S )   =>    |- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )
Theorem	caovcomg 5949*	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 5950*	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 5951*	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 5952*	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 5953*	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 5954*	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 5955*	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 5956*	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 5957*	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 5958*	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 5959*	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 5960*	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 5961*	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 5962*	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 5963*	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 5964*	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 5965*	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 5966*	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 5967*	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 5968*	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 5969*	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 5970*	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 5971*	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 5972*	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 5973*	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 5974*	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 5975*	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 5976*	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 5977*	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 5978*	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 5979*	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 5980*	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 5981*	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 5982*	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 5983*	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 5984*	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	caov4 5985*	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 ) )   &    |- D e. _V   =>    |- ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( B F D ) )
Theorem	caov411 5986*	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 ) )   &    |- D e. _V   =>    |- ( ( A F B ) F ( C F D ) ) = ( ( C F B ) F ( A F D ) )
Theorem	caov42 5987*	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 ) )   &    |- D e. _V   =>    |- ( ( A F B ) F ( C F D ) ) = ( ( A F C ) F ( D F B ) )
Theorem	caovdir 5988*	Reverse distributive law. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x G y ) = ( y G x )   &    |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) )   =>    |- ( ( A F B ) G C ) = ( ( A G C ) F ( B G C ) )
Theorem	caovdilem 5989*	Lemma used by real number construction. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x G y ) = ( y G x )   &    |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) )   &    |- D e. _V   &    |- H e. _V   &    |- ( ( x G y ) G z ) = ( x G ( y G z ) )   =>    |- ( ( ( A G C ) F ( B G D ) ) G H ) = ( ( A G ( C G H ) ) F ( B G ( D G H ) ) )
Theorem	caovlem2 5990*	Lemma used in real number construction. (Contributed by NM, 26-Aug-1995.)
|- A e. _V   &    |- B e. _V   &    |- C e. _V   &    |- ( x G y ) = ( y G x )   &    |- ( x G ( y F z ) ) = ( ( x G y ) F ( x G z ) )   &    |- D e. _V   &    |- H e. _V   &    |- ( ( x G y ) G z ) = ( x G ( y G z ) )   &    |- R e. _V   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   =>    |- ( ( ( ( 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	caovmo 5991*	Uniqueness of inverse element in commutative, associative operation with identity. Remark in proof of Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 4-Mar-1996.)
|- B e. S   &    |- dom F = ( S X. S )   &    |- -. (/) e. S   &    |- ( x F y ) = ( y F x )   &    |- ( ( x F y ) F z ) = ( x F ( y F z ) )   &    |- ( x e. S -> ( x F B ) = x )   =>    |- E* w ( A F w ) = B
Theorem	grprinvlem 5992*	Lemma for grprinvd 5993. (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 5993*	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 5994*	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.4.9  "Maps to" notation
Theorem	elmpt2cl 5995*	If a two-parameter class is not empty, 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	elmpt2cl1 5996*	If a two-parameter class is not empty, 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	elmpt2cl2 5997*	If a two-parameter class is not empty, 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	elovmpt2 5998*	Utility lemma for two-parameter classes. EDITORIAL: can simplify isghm 14646, islmhm 15747. (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	relmptopab 5999*	Any function to sets of ordered pairs produces a relation on function value unconditionally. (Contributed by Mario Carneiro, 7-Aug-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
|- F = ( x e. A |-> { <. y , z >. | ph } )   =>    |- Rel ( F ` B )
Theorem	f1ocnvd 6000*	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 ) ) )