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	$$⊢{\ll }_s=\left\{⟨a,b⟩|\left(a\subseteq \mathrm{No}\wedge b\subseteq \mathrm{No}\wedge \forall x\in a\forall y\in bx{<}_{s}y\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csslt	$$class{\ll }_s$$
1		va	$$setvara$$
2		vb	$$setvarb$$
3	1	cv	$$setvara$$
4		csur	$$class\mathrm{No}$$
5	3 4	wss	$$wffa\subseteq \mathrm{No}$$
6	2	cv	$$setvarb$$
7	6 4	wss	$$wffb\subseteq \mathrm{No}$$
8		vx	$$setvarx$$
9		vy	$$setvary$$
10	8	cv	$$setvarx$$
11		cslt	$$class{<}_s$$
12	9	cv	$$setvary$$
13	10 12 11	wbr	$$wffx{<}_{s}y$$
14	13 9 6	wral	$$wff\forall y\in bx{<}_{s}y$$
15	14 8 3	wral	$$wff\forall x\in a\forall y\in bx{<}_{s}y$$
16	5 7 15	w3a	$$wff\left(a\subseteq \mathrm{No}\wedge b\subseteq \mathrm{No}\wedge \forall x\in a\forall y\in bx{<}_{s}y\right)$$
17	16 1 2	copab	$$class\left\{⟨a,b⟩|\left(a\subseteq \mathrm{No}\wedge b\subseteq \mathrm{No}\wedge \forall x\in a\forall y\in bx{<}_{s}y\right)\right\}$$
18	0 17	wceq	$$wff{\ll }_s=\left\{⟨a,b⟩|\left(a\subseteq \mathrm{No}\wedge b\subseteq \mathrm{No}\wedge \forall x\in a\forall y\in bx{<}_{s}y\right)\right\}$$