HomeHome Intuitionistic Logic Explorer
Theorem List (p. 57 of 102)
< Previous  Next >
Browser slow? Try the
Unicode version.

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

Theorem List for Intuitionistic Logic Explorer - 5601-5700   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremfunoprab 5601* "At most one" is a sufficient condition for an operation class abstraction to be a function. (Contributed by NM, 17-Mar-1995.)
 |- 
 E* z ph   =>    |- 
 Fun  { <. <. x ,  y >. ,  z >.  |  ph }
 
Theoremfnoprabg 5602* Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007.)
 |-  ( A. x A. y ( ph  ->  E! z ps )  ->  { <. <. x ,  y >. ,  z >.  |  (
 ph  /\  ps ) }  Fn  { <. x ,  y >.  |  ph } )
 
Theoremmpt2fun 5603* The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   =>    |-  Fun  F
 
Theoremfnoprab 5604* Functionality and domain of an operation class abstraction. (Contributed by NM, 15-May-1995.)
 |-  ( ph  ->  E! z ps )   =>    |- 
 { <. <. x ,  y >. ,  z >.  |  (
 ph  /\  ps ) }  Fn  { <. x ,  y >.  |  ph }
 
Theoremffnov 5605* An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004.)
 |-  ( F : ( A  X.  B ) --> C  <->  ( F  Fn  ( A  X.  B ) 
 /\  A. x  e.  A  A. y  e.  B  ( x F y )  e.  C ) )
 
Theoremfovcl 5606 Closure law for an operation. (Contributed by NM, 19-Apr-2007.)
 |-  F : ( R  X.  S ) --> C   =>    |-  ( ( A  e.  R  /\  B  e.  S )  ->  ( A F B )  e.  C )
 
Theoremeqfnov 5607* Equality of two operations is determined by their values. (Contributed by NM, 1-Sep-2005.)
 |-  ( ( F  Fn  ( A  X.  B ) 
 /\  G  Fn  ( C  X.  D ) ) 
 ->  ( F  =  G  <->  ( ( A  X.  B )  =  ( C  X.  D )  /\  A. x  e.  A  A. y  e.  B  ( x F y )  =  ( x G y ) ) ) )
 
Theoremeqfnov2 5608* Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010.)
 |-  ( ( F  Fn  ( A  X.  B ) 
 /\  G  Fn  ( A  X.  B ) ) 
 ->  ( F  =  G  <->  A. x  e.  A  A. y  e.  B  ( x F y )  =  ( x G y ) ) )
 
Theoremfnovim 5609* Representation of a function in terms of its values. (Contributed by Jim Kingdon, 16-Jan-2019.)
 |-  ( F  Fn  ( A  X.  B )  ->  F  =  ( x  e.  A ,  y  e.  B  |->  ( x F y ) ) )
 
Theoremmpt22eqb 5610* Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnov2 5608. (Contributed by Mario Carneiro, 4-Jan-2017.)
 |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  ( ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )  <->  A. x  e.  A  A. y  e.  B  C  =  D ) )
 
Theoremrnmpt2 5611* The range of an operation given by the "maps to" notation. (Contributed by FL, 20-Jun-2011.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   =>    |-  ran  F  =  { z  |  E. x  e.  A  E. y  e.  B  z  =  C }
 
Theoremreldmmpt2 5612* The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   =>    |-  Rel  dom  F
 
Theoremelrnmpt2g 5613* Membership in the range of an operation class abstraction. (Contributed by NM, 27-Aug-2007.) (Revised by Mario Carneiro, 31-Aug-2015.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   =>    |-  ( D  e.  V  ->  ( D  e.  ran 
 F 
 <-> 
 E. x  e.  A  E. y  e.  B  D  =  C )
 )
 
Theoremelrnmpt2 5614* Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 31-Aug-2015.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   &    |-  C  e.  _V   =>    |-  ( D  e.  ran  F  <->  E. x  e.  A  E. y  e.  B  D  =  C )
 
Theoremralrnmpt2 5615* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   &    |-  (
 z  =  C  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  ( A. z  e. 
 ran  F ph  <->  A. x  e.  A  A. y  e.  B  ps ) )
 
Theoremrexrnmpt2 5616* A restricted quantifier over an image set. (Contributed by Mario Carneiro, 1-Sep-2015.)
 |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )   &    |-  (
 z  =  C  ->  (
 ph 
 <->  ps ) )   =>    |-  ( A. x  e.  A  A. y  e.  B  C  e.  V  ->  ( E. z  e. 
 ran  F ph  <->  E. x  e.  A  E. y  e.  B  ps ) )
 
Theoremovid 5617* The value of an operation class abstraction. (Contributed by NM, 16-May-1995.) (Revised by David Abernethy, 19-Jun-2012.)
 |-  ( ( x  e.  R  /\  y  e.  S )  ->  E! z ph )   &    |-  F  =  { <.
 <. x ,  y >. ,  z >.  |  (
 ( x  e.  R  /\  y  e.  S )  /\  ph ) }   =>    |-  ( ( x  e.  R  /\  y  e.  S )  ->  (
 ( x F y )  =  z  <->  ph ) )
 
Theoremovidig 5618* The value of an operation class abstraction. Compare ovidi 5619. The condition  ( x  e.  R  /\  y  e.  S ) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014.)
 |- 
 E* z ph   &    |-  F  =  { <.
 <. x ,  y >. ,  z >.  |  ph }   =>    |-  ( ph  ->  ( x F y )  =  z )
 
Theoremovidi 5619* The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014.)
 |-  ( ( x  e.  R  /\  y  e.  S )  ->  E* z ph )   &    |-  F  =  { <.
 <. x ,  y >. ,  z >.  |  (
 ( x  e.  R  /\  y  e.  S )  /\  ph ) }   =>    |-  ( ( x  e.  R  /\  y  e.  S )  ->  ( ph  ->  ( x F y )  =  z ) )
 
Theoremov 5620* 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 ) )
 
Theoremovigg 5621* The value of an operation class abstraction. Compare ovig 5622. 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 )
 )
 
Theoremovig 5622* 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 )
 )
 
Theoremovmpt4g 5623* Value of a function given by the "maps to" notation. (This is the operation analog of fvmpt2 5254.) (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 )
 
Theoremovmpt2s 5624* 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 )
 
Theoremov2gf 5625* The value of an operation class abstraction. A version of ovmpt2g 5635 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 )
 
Theoremovmpt2dxf 5626* 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 )
 
Theoremovmpt2dx 5627* 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 )
 
Theoremovmpt2d 5628* 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 )
 
Theoremovmpt2x 5629* The value of an operation class abstraction. Variant of ovmpt2ga 5630 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 )
 
Theoremovmpt2ga 5630* 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 )
 
Theoremovmpt2a 5631* 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 )
 
Theoremovmpt2df 5632* Alternate deduction version of ovmpt2 5636, 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 ) )
 
Theoremovmpt2dv 5633* Alternate deduction version of ovmpt2 5636, 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 ) )
 
Theoremovmpt2dv2 5634* Alternate deduction version of ovmpt2 5636, 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 ) )
 
Theoremovmpt2g 5635* 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 )
 
Theoremovmpt2 5636* 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 )
 
Theoremovi3 5637* The value of an operation class abstraction. Special case. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 29-Dec-2014.)
 |-  ( ( ( A  e.  H  /\  B  e.  H )  /\  ( C  e.  H  /\  D  e.  H )
 )  ->  S  e.  ( H  X.  H ) )   &    |-  ( ( ( 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 )
 
Theoremov6g 5638* 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 )
 
Theoremovg 5639* 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 ) )
 
Theoremovres 5640 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 ) )
 
Theoremovresd 5641 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 ) )
 
Theoremoprssov 5642 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 ) )
 
Theoremfovrn 5643 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 )
 
Theoremfovrnda 5644 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 )
 
Theoremfovrnd 5645 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 )
 
Theoremfnrnov 5646* 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 ) }
 )
 
Theoremfoov 5647* 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 ) ) )
 
Theoremfnovrn 5648 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 )
 
Theoremovelrn 5649* 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 ) ) )
 
Theoremfunimassov 5650* 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 ) )
 
Theoremovelimab 5651* 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 ) ) )
 
Theoremovconst2 5652 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 )
 
Theoremcaovclg 5653* 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 )
 
Theoremcaovcld 5654* 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 )
 
Theoremcaovcl 5655* 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 )
 
Theoremcaovcomg 5656* 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 ) )
 
Theoremcaovcomd 5657* 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 ) )
 
Theoremcaovcom 5658* 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 )
 
Theoremcaovassg 5659* 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 ) ) )
 
Theoremcaovassd 5660* 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 ) ) )
 
Theoremcaovass 5661* 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 ) )
 
Theoremcaovcang 5662* 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 ) )
 
Theoremcaovcand 5663* 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 ) )
 
Theoremcaovcanrd 5664* 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 ) )
 
Theoremcaovcan 5665* 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 ) )
 
Theoremcaovordig 5666* 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 ) ) )
 
Theoremcaovordid 5667* 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 ) ) )
 
Theoremcaovordg 5668* 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 ) ) )
 
Theoremcaovordd 5669* 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 ) ) )
 
Theoremcaovord2d 5670* 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 ) ) )
 
Theoremcaovord3d 5671* 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 ) ) )
 
Theoremcaovord 5672* 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 ) ) )
 
Theoremcaovord2 5673* 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 ) ) )
 
Theoremcaovord3 5674* 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 ) )
 
Theoremcaovdig 5675* 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 ) ) )
 
Theoremcaovdid 5676* 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 ) ) )
 
Theoremcaovdir2d 5677* 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 ) ) )
 
Theoremcaovdirg 5678* 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 ) ) )
 
Theoremcaovdird 5679* 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 ) ) )
 
Theoremcaovdi 5680* 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 ) )
 
Theoremcaov32d 5681* 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 ) )
 
Theoremcaov12d 5682* 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 ) ) )
 
Theoremcaov31d 5683* 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 ) )
 
Theoremcaov13d 5684* 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 ) ) )
 
Theoremcaov4d 5685* 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 ) ) )
 
Theoremcaov411d 5686* 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 ) ) )
 
Theoremcaov42d 5687* 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 ) ) )
 
Theoremcaov32 5688* 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 )
 
Theoremcaov12 5689* 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 ) )
 
Theoremcaov31 5690* 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 )
 
Theoremcaov13 5691* 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 ) )
 
Theoremcaovdilemd 5692* 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 ) ) ) )
 
Theoremcaovlem2d 5693* 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 ) ) ) ) )
 
Theoremcaovimo 5694* 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 ) )
 
Theoremgrprinvlem 5695* Lemma for grprinvd 5696. (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 )
 
Theoremgrprinvd 5696* 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 )
 
Theoremgrpridd 5697* Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
 |-  ( ( ph  /\  x  e.  B  /\  y  e.  B )  ->  ( x  .+  y )  e.  B )   &    |-  ( ph  ->  O  e.  B )   &    |-  (
 ( ph  /\  x  e.  B )  ->  ( O  .+  x )  =  x )   &    |-  ( ( ph  /\  ( x  e.  B  /\  y  e.  B  /\  z  e.  B ) )  ->  ( ( x  .+  y ) 
 .+  z )  =  ( x  .+  (
 y  .+  z )
 ) )   &    |-  ( ( ph  /\  x  e.  B ) 
 ->  E. y  e.  B  ( y  .+  x )  =  O )   =>    |-  ( ( ph  /\  x  e.  B ) 
 ->  ( x  .+  O )  =  x )
 
2.6.11  "Maps to" notation
 
Theoremelmpt2cl 5698* 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 ) )
 
Theoremelmpt2cl1 5699* 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 )
 
Theoremelmpt2cl2 5700* 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 )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
  Copyright terms: Public domain < Previous  Next >