Definition df-slt 31797

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

Assertion

Ref	Expression
df-slt	|- <s = { <. 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 ) ) ) }

Distinct variable group:   f, g, x, y

Detailed syntax breakdown of Definition df-slt

Step	Hyp	Ref	Expression
1		cslt 31794	. 2 class <s
2		vf	. . . . . . 7 setvar f
3	2	cv 1482	. . . . . 6 class f
4		csur 31793	. . . . . 6 class No
5	3, 4	wcel 1990	. . . . 5 wff f e. No
6		vg	. . . . . . 7 setvar g
7	6	cv 1482	. . . . . 6 class g
8	7, 4	wcel 1990	. . . . 5 wff g e. No
9	5, 8	wa 384	. . . 4 wff ( f e. No /\ g e. No )
10		vy	. . . . . . . . . 10 setvar y
11	10	cv 1482	. . . . . . . . 9 class y
12	11, 3	cfv 5888	. . . . . . . 8 class ( f ` y )
13	11, 7	cfv 5888	. . . . . . . 8 class ( g ` y )
14	12, 13	wceq 1483	. . . . . . 7 wff ( f ` y ) = ( g ` y )
15		vx	. . . . . . . 8 setvar x
16	15	cv 1482	. . . . . . 7 class x
17	14, 10, 16	wral 2912	. . . . . 6 wff A. y e. x ( f ` y ) = ( g ` y )
18	16, 3	cfv 5888	. . . . . . 7 class ( f ` x )
19	16, 7	cfv 5888	. . . . . . 7 class ( g ` x )
20		c1o 7553	. . . . . . . . 9 class 1o
21		c0 3915	. . . . . . . . 9 class (/)
22	20, 21	cop 4183	. . . . . . . 8 class <. 1o , (/) >.
23		c2o 7554	. . . . . . . . 9 class 2o
24	20, 23	cop 4183	. . . . . . . 8 class <. 1o , 2o >.
25	21, 23	cop 4183	. . . . . . . 8 class <. (/) , 2o >.
26	22, 24, 25	ctp 4181	. . . . . . 7 class { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. }
27	18, 19, 26	wbr 4653	. . . . . 6 wff ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x )
28	17, 27	wa 384	. . . . 5 wff ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) )
29		con0 5723	. . . . 5 class On
30	28, 15, 29	wrex 2913	. . . 4 wff E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) )
31	9, 30	wa 384	. . 3 wff ( ( 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	31, 2, 6	copab 4712	. 2 class { <. 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 ) ) ) }
33	1, 32	wceq 1483	1 wff <s = { <. 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 ) ) ) }

This definition is referenced by:  sltval  31800  sltso  31827