Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sslt Structured version   Visualization version   GIF version

Definition df-sslt 32230
 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
StepHypRef Expression
1 csslt 32229 . 2 class <<s
2 va . . . . . 6 setvar 𝑎
32cv 1630 . . . . 5 class 𝑎
4 csur 32126 . . . . 5 class No
53, 4wss 3723 . . . 4 wff 𝑎 No
6 vb . . . . . 6 setvar 𝑏
76cv 1630 . . . . 5 class 𝑏
87, 4wss 3723 . . . 4 wff 𝑏 No
9 vx . . . . . . . 8 setvar 𝑥
109cv 1630 . . . . . . 7 class 𝑥
11 vy . . . . . . . 8 setvar 𝑦
1211cv 1630 . . . . . . 7 class 𝑦
13 cslt 32127 . . . . . . 7 class <s
1410, 12, 13wbr 4786 . . . . . 6 wff 𝑥 <s 𝑦
1514, 11, 7wral 3061 . . . . 5 wff 𝑦𝑏 𝑥 <s 𝑦
1615, 9, 3wral 3061 . . . 4 wff 𝑥𝑎𝑦𝑏 𝑥 <s 𝑦
175, 8, 16w3a 1071 . . 3 wff (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)
1817, 2, 6copab 4846 . 2 class {⟨𝑎, 𝑏⟩ ∣ (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)}
191, 18wceq 1631 1 wff <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  brsslt  32233  dmscut  32251
 Copyright terms: Public domain W3C validator