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 33279
 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 33276 . 2 class <s
2 vf . . . . . . 7 setvar 𝑓
32cv 1537 . . . . . 6 class 𝑓
4 csur 33275 . . . . . 6 class No
53, 4wcel 2111 . . . . 5 wff 𝑓 No
6 vg . . . . . . 7 setvar 𝑔
76cv 1537 . . . . . 6 class 𝑔
87, 4wcel 2111 . . . . 5 wff 𝑔 No
95, 8wa 399 . . . 4 wff (𝑓 No 𝑔 No )
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1537 . . . . . . . . 9 class 𝑦
1211, 3cfv 6325 . . . . . . . 8 class (𝑓𝑦)
1311, 7cfv 6325 . . . . . . . 8 class (𝑔𝑦)
1412, 13wceq 1538 . . . . . . 7 wff (𝑓𝑦) = (𝑔𝑦)
15 vx . . . . . . . 8 setvar 𝑥
1615cv 1537 . . . . . . 7 class 𝑥
1714, 10, 16wral 3106 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑔𝑦)
1816, 3cfv 6325 . . . . . . 7 class (𝑓𝑥)
1916, 7cfv 6325 . . . . . . 7 class (𝑔𝑥)
20 c1o 8081 . . . . . . . . 9 class 1o
21 c0 4243 . . . . . . . . 9 class
2220, 21cop 4531 . . . . . . . 8 class ⟨1o, ∅⟩
23 c2o 8082 . . . . . . . . 9 class 2o
2420, 23cop 4531 . . . . . . . 8 class ⟨1o, 2o
2521, 23cop 4531 . . . . . . . 8 class ⟨∅, 2o
2622, 24, 25ctp 4529 . . . . . . 7 class {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}
2718, 19, 26wbr 5031 . . . . . 6 wff (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)
2817, 27wa 399 . . . . 5 wff (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))
29 con0 6160 . . . . 5 class On
3028, 15, 29wrex 3107 . . . 4 wff 𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥))
319, 30wa 399 . . 3 wff ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))
3231, 2, 6copab 5093 . 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
331, 32wceq 1538 1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
 Colors of variables: wff setvar class This definition is referenced by:  sltval  33282  sltso  33309
 Copyright terms: Public domain W3C validator