Definition df-slts

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cslts	⊢ <<s
1		va	⊢ 𝑎
2		vb	⊢ 𝑏
3	1	cv	⊢ 𝑎
4		csur	⊢ No
5	3 4	wss	⊢ 𝑎 ⊆ No
6	2	cv	⊢ 𝑏
7	6 4	wss	⊢ 𝑏 ⊆ No
8		vx	⊢ 𝑥
9		vy	⊢ 𝑦
10	8	cv	⊢ 𝑥
11		clts	⊢ <s
12	9	cv	⊢ 𝑦
13	10 12 11	wbr	⊢ 𝑥 <s 𝑦
14	13 9 6	wral	⊢ ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦
15	14 8 3	wral	⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦
16	5 7 15	w3a	⊢ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 )
17	16 1 2	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) }
18	0 17	wceq	⊢ <<s = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) }