P. 69 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 6801-6900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ovresd 6801	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	oprres 6802*	The restriction of an operation is an operation. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 19-Oct-2021.)
|- ( ( ph /\ x e. Y /\ y e. Y ) -> ( x F y ) = ( x G y ) )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> F : ( Y X. Y ) --> R )   &    |- ( ph -> G : ( X X. X ) --> S )   =>    |- ( ph -> F = ( G |` ( Y X. Y ) ) )
Theorem	oprssov 6803	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 6804	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 6805	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 6806	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 6807*	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 6808*	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 6809	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 6810*	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 6811*	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 6812*	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	ovima0 6813	An operation value is a member of the image plus null. (Contributed by Thierry Arnoux, 25-Jun-2019.)
|- ( ( X e. A /\ Y e. B ) -> ( X R Y ) e. ( ( R " ( A X. B ) ) u. { (/) } ) )
Theorem	ovconst2 6814	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	oprssdm 6815*	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	nssdmovg 6816	The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017.)
|- ( ( dom F C_ ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> ( A F B ) = (/) )
Theorem	ndmovg 6817	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 6818	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 6819	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 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 6820	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 6821	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 6822	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 6823	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 6824	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 6825	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 6826*	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 6827*	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 6828*	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 6829*	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 6830*	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 6831*	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 6832*	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 6833*	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 6834*	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 6835*	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 6836*	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 6837*	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 6838*	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 6839*	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 6840*	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 6841*	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 6842*	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 6843*	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 6844*	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 6845*	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 6846*	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 6847*	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 6848*	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 6849*	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 6850*	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 6851*	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 6852*	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 6853*	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 6854*	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 6855*	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 6856*	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 6857*	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 6858*	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 6859*	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 6860*	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 6861*	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 6862*	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 6863*	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 6864*	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 6865*	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 6866*	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 6867*	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 6868*	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 6869*	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 6870*	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 6871*	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 6872*	Lemma for grprinvd 6873. (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 6873*	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 6874*	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.3.19  "Maps to" notation
Theorem	mpt2ndm0 6875*	The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
|- F = ( x e. X , y e. Y |-> C )   =>    |- ( -. ( V e. X /\ W e. Y ) -> ( V F W ) = (/) )
Theorem	elmpt2cl 6876*	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 6877*	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 6878*	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 6879*	Utility lemma for two-parameter classes. EDITORIAL: can simplify isghm 17660, islmhm 19027. (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	elovmpt2rab 6880*	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	elovmpt2rab1 6881*	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.)
|- 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	2mpt20 6882*	If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021.)
|- O = ( x e. A , y e. B |-> E )   &    |- ( ( X e. A /\ Y e. B ) -> ( X O Y ) = ( s e. C , t e. D |-> F ) )   =>    |- ( -. ( ( X e. A /\ Y e. B ) /\ ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = (/) )
Theorem	relmptopab 6883*	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 6884*	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 6885*	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 6886*	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 6887*	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 6888*	A one-to-one mapping induces a one-to-one mapping on power sets. This version of f1opw 6889 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 6889*	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	elovmpt3imp 6890*	If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands must be sets. Remark: a function which is the result of an operation can be regared as operation with 3 operands - therefore the abbreviation "mpt3" is used in the label. (Contributed by AV, 16-May-2019.)
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> B ) )   =>    |- ( A e. ( ( X O Y ) ` Z ) -> ( X e. _V /\ Y e. _V ) )
Theorem	ovmpt3rab1 6891*	The value of an operation defined by the maps-to notation with a function into a class abstraction as a result. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )   &    |- ( ( x = X /\ y = Y ) -> M = K )   &    |- ( ( x = X /\ y = Y ) -> N = L )   &    |- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )   &    |- F/ x ps   &    |- F/ y ps   =>    |- ( ( X e. V /\ Y e. W /\ K e. U ) -> ( X O Y ) = ( z e. K |-> { a e. L | ps } ) )
Theorem	ovmpt3rabdm 6892*	If the value of a function which is the result of an operation defined by the maps-to notation is not empty, the operands and the argument of the function must be sets. (Contributed by AV, 16-May-2019.)
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )   &    |- ( ( x = X /\ y = Y ) -> M = K )   &    |- ( ( x = X /\ y = Y ) -> N = L )   =>    |- ( ( ( X e. V /\ Y e. W /\ K e. U ) /\ L e. T ) -> dom ( X O Y ) = K )
Theorem	elovmpt3rab1 6893*	Implications for the value of an operation defined by the maps-to notation with a function into a class abstraction as a result having an element. The domain of the function and the base set of the class abstraction may depend on the operands, using implicit substitution. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )   &    |- ( ( x = X /\ y = Y ) -> M = K )   &    |- ( ( x = X /\ y = Y ) -> N = L )   =>    |- ( ( K e. U /\ L e. T ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. K /\ A e. L ) ) ) )
Theorem	elovmpt3rab 6894*	Implications for the value of an operation defined by the maps-to notation with a class abstration as a result having an element. (Contributed by AV, 17-Jul-2018.) (Revised by AV, 16-May-2019.)
|- O = ( x e. _V , y e. _V |-> ( z e. M |-> { a e. N | ph } ) )   =>    |- ( ( M e. U /\ N e. T ) -> ( A e. ( ( X O Y ) ` Z ) -> ( ( X e. _V /\ Y e. _V ) /\ ( Z e. M /\ A e. N ) ) ) )
2.3.20  Function operation
Syntax	cof 6895	Extend class notation to include mapping of an operation to a function operation.
class oF R
Syntax	cofr 6896	Extend class notation to include mapping of a binary relation to a function relation.
class oR R
Definition	df-of 6897*	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 6898*	Define the function relation map. The definition is designed so that if R is a binary relation, then oR 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 6899	Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014.)
|- ( R = S -> oF R = oF S )
Theorem	ofreq 6900	Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014.)
|- ( R = S -> oR R = oR S )