Definition df-sslt

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

	Ref	Expression
Assertion	df-sslt	|- <. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csslt	|- <
1		va	|- a
2		vb	|- b
3	1	cv	|- a
4		csur	|- No
5	3 4	wss	|- a C_ No
6	2	cv	|- b
7	6 4	wss	|- b C_ No
8		vx	|- x
9		vy	|- y
10	8	cv	|- x
11		cslt	|-
12	9	cv	|- y
13	10 12 11	wbr	|- x
14	13 9 6	wral	|- A. y e. b x
15	14 8 3	wral	|- A. x e. a A. y e. b x
16	5 7 15	w3a	|- ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x
17	16 1 2	copab	|- { <. a , b >. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x
18	0 17	wceq	|- <. | ( a C_ No /\ b C_ No /\ A. x e. a A. y e. b x