Metamath Proof Explorer


Definition df-sslt

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

Ref Expression
Assertion df-sslt <<s = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 No 𝑏 No ∧ ∀ 𝑥𝑎𝑦𝑏 𝑥 <s 𝑦 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csslt <<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 cslt <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 𝑦 ) }