Users' Mathboxes 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 32223
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 32222 . 2 class <<s
2 va . . . . . 6 setvar 𝑎
32cv 1636 . . . . 5 class 𝑎
4 csur 32119 . . . . 5 class No
53, 4wss 3776 . . . 4 wff 𝑎 No
6 vb . . . . . 6 setvar 𝑏
76cv 1636 . . . . 5 class 𝑏
87, 4wss 3776 . . . 4 wff 𝑏 No
9 vx . . . . . . . 8 setvar 𝑥
109cv 1636 . . . . . . 7 class 𝑥
11 vy . . . . . . . 8 setvar 𝑦
1211cv 1636 . . . . . . 7 class 𝑦
13 cslt 32120 . . . . . . 7 class <s
1410, 12, 13wbr 4851 . . . . . 6 wff 𝑥 <s 𝑦
1514, 11, 7wral 3103 . . . . 5 wff 𝑦𝑏 𝑥 <s 𝑦
1615, 9, 3wral 3103 . . . 4 wff 𝑥𝑎𝑦𝑏 𝑥 <s 𝑦
175, 8, 16w3a 1100 . . 3 wff (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)
1817, 2, 6copab 4913 . 2 class {⟨𝑎, 𝑏⟩ ∣ (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)}
191, 18wceq 1637 1 wff <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  brsslt  32226  dmscut  32244
  Copyright terms: Public domain W3C validator