Definition df-sslt 33251

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 = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)}

Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Detailed syntax breakdown of Definition df-sslt

Step	Hyp	Ref	Expression
1		csslt 33250	. 2 class <<s
2		va	. . . . . 6 setvar 𝑎
3	2	cv 1536	. . . . 5 class 𝑎
4		csur 33147	. . . . 5 class No
5	3, 4	wss 3936	. . . 4 wff 𝑎 ⊆ No
6		vb	. . . . . 6 setvar 𝑏
7	6	cv 1536	. . . . 5 class 𝑏
8	7, 4	wss 3936	. . . 4 wff 𝑏 ⊆ No
9		vx	. . . . . . . 8 setvar 𝑥
10	9	cv 1536	. . . . . . 7 class 𝑥
11		vy	. . . . . . . 8 setvar 𝑦
12	11	cv 1536	. . . . . . 7 class 𝑦
13		cslt 33148	. . . . . . 7 class <s
14	10, 12, 13	wbr 5066	. . . . . 6 wff 𝑥 <s 𝑦
15	14, 11, 7	wral 3138	. . . . 5 wff ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦
16	15, 9, 3	wral 3138	. . . 4 wff ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦
17	5, 8, 16	w3a 1083	. . 3 wff (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)
18	17, 2, 6	copab 5128	. 2 class {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)}
19	1, 18	wceq 1537	1 wff <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥 <s 𝑦)}

This definition is referenced by:  brsslt  33254  dmscut  33272