Metamath Proof Explorer

Definition df-slt

Description: Next, we introduce surreal less-than, a comparison relation over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011)

Ref Expression
Assertion df-slt 
|- . | ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cslt 
 |-
1 vf 
 |-  f
2 vg 
 |-  g
3 1 cv 
 |-  f
4 csur 
 |-  No
5 3 4 wcel 
 |-  f e. No
6 2 cv 
 |-  g
7 6 4 wcel 
 |-  g e. No
8 5 7 wa 
 |-  ( f e. No /\ g e. No )
9 vx 
 |-  x
10 con0 
 |-  On
11 vy 
 |-  y
12 9 cv 
 |-  x
13 11 cv 
 |-  y
14 13 3 cfv 
 |-  ( f ` y )
15 13 6 cfv 
 |-  ( g ` y )
16 14 15 wceq 
 |-  ( f ` y ) = ( g ` y )
17 16 11 12 wral 
 |-  A. y e. x ( f ` y ) = ( g ` y )
18 12 3 cfv 
 |-  ( f ` x )
19 c1o 
 |-  1o
20 c0 
 |-  (/)
21 19 20 cop 
 |-  <. 1o , (/) >.
22 c2o 
 |-  2o
23 19 22 cop 
 |-  <. 1o , 2o >.
24 20 22 cop 
 |-  <. (/) , 2o >.
25 21 23 24 ctp 
 |-  { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. }
26 12 6 cfv 
 |-  ( g ` x )
27 18 26 25 wbr 
 |-  ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x )
28 17 27 wa 
 |-  ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) )
29 28 9 10 wrex 
 |-  E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) )
30 8 29 wa 
 |-  ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) )
31 30 1 2 copab 
 |-  { <. f , g >. | ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) }
32 0 31 wceq 
 |-  . | ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) }