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

Definition df-slt 33048
Description: Next, we introduce surreal less-than, a comparison relationship over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.)
Assertion
Ref Expression
df-slt <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
Distinct variable group:   𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-slt
StepHypRef Expression
1 cslt 33045 . 2 class <s
2 vf . . . . . . 7 setvar 𝑓
32cv 1527 . . . . . 6 class 𝑓
4 csur 33044 . . . . . 6 class No
53, 4wcel 2105 . . . . 5 wff 𝑓 No
6 vg . . . . . . 7 setvar 𝑔
76cv 1527 . . . . . 6 class 𝑔
87, 4wcel 2105 . . . . 5 wff 𝑔 No
95, 8wa 396 . . . 4 wff (𝑓 No 𝑔 No )
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1527 . . . . . . . . 9 class 𝑦
1211, 3cfv 6348 . . . . . . . 8 class (𝑓𝑦)
1311, 7cfv 6348 . . . . . . . 8 class (𝑔𝑦)
1412, 13wceq 1528 . . . . . . 7 wff (𝑓𝑦) = (𝑔𝑦)
15 vx . . . . . . . 8 setvar 𝑥
1615cv 1527 . . . . . . 7 class 𝑥
1714, 10, 16wral 3135 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑔𝑦)
1816, 3cfv 6348 . . . . . . 7 class (𝑓𝑥)
1916, 7cfv 6348 . . . . . . 7 class (𝑔𝑥)
20 c1o 8084 . . . . . . . . 9 class 1o
21 c0 4288 . . . . . . . . 9 class
2220, 21cop 4563 . . . . . . . 8 class ⟨1o, ∅⟩
23 c2o 8085 . . . . . . . . 9 class 2o
2420, 23cop 4563 . . . . . . . 8 class ⟨1o, 2o
2521, 23cop 4563 . . . . . . . 8 class ⟨∅, 2o
2622, 24, 25ctp 4561 . . . . . . 7 class {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}
2718, 19, 26wbr 5057 . . . . . 6 wff (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)
2817, 27wa 396 . . . . 5 wff (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))
29 con0 6184 . . . . 5 class On
3028, 15, 29wrex 3136 . . . 4 wff 𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))
319, 30wa 396 . . 3 wff ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))
3231, 2, 6copab 5119 . 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
331, 32wceq 1528 1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  sltval  33051  sltso  33078
  Copyright terms: Public domain W3C validator