Definition df-sslt 31897

Description: Define the relationship that holds iff one set of surreals completely precedes another. (Contributed by Scott Fenton, 7-Dec-2021.)

Assertion

Ref	Expression
df-sslt	|- < <s = { <. a , b >. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x <s y ) }

Distinct variable group:   a, b, x, y

Detailed syntax breakdown of Definition df-sslt

Step	Hyp	Ref	Expression
1		csslt 31896	. 2 class < <s
2		va	. . . . . 6 setvar a
3	2	cv 1482	. . . . 5 class a
4		csur 31793	. . . . 5 class No
5	3, 4	wss 3574	. . . 4 wff a C_ No
6		vb	. . . . . 6 setvar b
7	6	cv 1482	. . . . 5 class b
8	7, 4	wss 3574	. . . 4 wff b C_ No
9		vx	. . . . . . . 8 setvar x
10	9	cv 1482	. . . . . . 7 class x
11		vy	. . . . . . . 8 setvar y
12	11	cv 1482	. . . . . . 7 class y
13		cslt 31794	. . . . . . 7 class <s
14	10, 12, 13	wbr 4653	. . . . . 6 wff x <s y
15	14, 11, 7	wral 2912	. . . . 5 wff A. y e. b x <s y
16	15, 9, 3	wral 2912	. . . 4 wff A. x e. a A. y e. b x <s y
17	5, 8, 16	w3a 1037	. . 3 wff ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x <s y )
18	17, 2, 6	copab 4712	. 2 class { <. a , b >. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x <s y ) }
19	1, 18	wceq 1483	1 wff < <s = { <. a , b >. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x <s y ) }

This definition is referenced by:  brsslt  31900  dmscut  31918