Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tofld Unicode version

Definition df-tofld 25440
Description: Definition of a totally ordered field. Experimental. (Contributed by FL, 27-Jun-2011.)
Assertion
Ref Expression
df-tofld  |-  Tofld  =  { <. <. g ,  h >. ,  r >.  |  (
<. g ,  h >.  e. 
Fld  /\  ( r  e. 
TosetRel  /\  U. U. r  =  ran  g )  /\  A. x  e.  U. U. r A. y  e.  U. U. r A. z  e. 
U. U. r ( ( x r y  -> 
( x g z ) r ( y g z ) )  /\  ( (GId `  g ) r z  ->  ( x h z ) r ( y h z ) ) ) ) }
Distinct variable group:    g, h, r, x, y, z

Detailed syntax breakdown of Definition df-tofld
StepHypRef Expression
1 ctofld 25439 . 2  class  Tofld
2 vg . . . . . . 7  set  g
32cv 1622 . . . . . 6  class  g
4 vh . . . . . . 7  set  h
54cv 1622 . . . . . 6  class  h
63, 5cop 3643 . . . . 5  class  <. g ,  h >.
7 cfld 21080 . . . . 5  class  Fld
86, 7wcel 1684 . . . 4  wff  <. g ,  h >.  e.  Fld
9 vr . . . . . . 7  set  r
109cv 1622 . . . . . 6  class  r
11 ctsr 14302 . . . . . 6  class  TosetRel
1210, 11wcel 1684 . . . . 5  wff  r  e.  TosetRel
1310cuni 3827 . . . . . . 7  class  U. r
1413cuni 3827 . . . . . 6  class  U. U. r
153crn 4690 . . . . . 6  class  ran  g
1614, 15wceq 1623 . . . . 5  wff  U. U. r  =  ran  g
1712, 16wa 358 . . . 4  wff  ( r  e.  TosetRel  /\  U. U. r  =  ran  g )
18 vx . . . . . . . . . . 11  set  x
1918cv 1622 . . . . . . . . . 10  class  x
20 vy . . . . . . . . . . 11  set  y
2120cv 1622 . . . . . . . . . 10  class  y
2219, 21, 10wbr 4023 . . . . . . . . 9  wff  x r y
23 vz . . . . . . . . . . . 12  set  z
2423cv 1622 . . . . . . . . . . 11  class  z
2519, 24, 3co 5858 . . . . . . . . . 10  class  ( x g z )
2621, 24, 3co 5858 . . . . . . . . . 10  class  ( y g z )
2725, 26, 10wbr 4023 . . . . . . . . 9  wff  ( x g z ) r ( y g z )
2822, 27wi 4 . . . . . . . 8  wff  ( x r y  ->  (
x g z ) r ( y g z ) )
29 cgi 20854 . . . . . . . . . . 11  class GId
303, 29cfv 5255 . . . . . . . . . 10  class  (GId `  g )
3130, 24, 10wbr 4023 . . . . . . . . 9  wff  (GId `  g ) r z
3219, 24, 5co 5858 . . . . . . . . . 10  class  ( x h z )
3321, 24, 5co 5858 . . . . . . . . . 10  class  ( y h z )
3432, 33, 10wbr 4023 . . . . . . . . 9  wff  ( x h z ) r ( y h z )
3531, 34wi 4 . . . . . . . 8  wff  ( (GId
`  g ) r z  ->  ( x h z ) r ( y h z ) )
3628, 35wa 358 . . . . . . 7  wff  ( ( x r y  -> 
( x g z ) r ( y g z ) )  /\  ( (GId `  g ) r z  ->  ( x h z ) r ( y h z ) ) )
3736, 23, 14wral 2543 . . . . . 6  wff  A. z  e.  U. U. r ( ( x r y  ->  ( x g z ) r ( y g z ) )  /\  ( (GId
`  g ) r z  ->  ( x h z ) r ( y h z ) ) )
3837, 20, 14wral 2543 . . . . 5  wff  A. y  e.  U. U. r A. z  e.  U. U. r
( ( x r y  ->  ( x
g z ) r ( y g z ) )  /\  (
(GId `  g )
r z  ->  (
x h z ) r ( y h z ) ) )
3938, 18, 14wral 2543 . . . 4  wff  A. x  e.  U. U. r A. y  e.  U. U. r A. z  e.  U. U. r ( ( x r y  ->  (
x g z ) r ( y g z ) )  /\  ( (GId `  g )
r z  ->  (
x h z ) r ( y h z ) ) )
408, 17, 39w3a 934 . . 3  wff  ( <.
g ,  h >.  e. 
Fld  /\  ( r  e. 
TosetRel  /\  U. U. r  =  ran  g )  /\  A. x  e.  U. U. r A. y  e.  U. U. r A. z  e. 
U. U. r ( ( x r y  -> 
( x g z ) r ( y g z ) )  /\  ( (GId `  g ) r z  ->  ( x h z ) r ( y h z ) ) ) )
4140, 2, 4, 9coprab 5859 . 2  class  { <. <.
g ,  h >. ,  r >.  |  ( <. g ,  h >.  e. 
Fld  /\  ( r  e. 
TosetRel  /\  U. U. r  =  ran  g )  /\  A. x  e.  U. U. r A. y  e.  U. U. r A. z  e. 
U. U. r ( ( x r y  -> 
( x g z ) r ( y g z ) )  /\  ( (GId `  g ) r z  ->  ( x h z ) r ( y h z ) ) ) ) }
421, 41wceq 1623 1  wff  Tofld  =  { <. <. g ,  h >. ,  r >.  |  (
<. g ,  h >.  e. 
Fld  /\  ( r  e. 
TosetRel  /\  U. U. r  =  ran  g )  /\  A. x  e.  U. U. r A. y  e.  U. U. r A. z  e. 
U. U. r ( ( x r y  -> 
( x g z ) r ( y g z ) )  /\  ( (GId `  g ) r z  ->  ( x h z ) r ( y h z ) ) ) ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator