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 31041
 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 (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
Distinct variable group:   𝑓,𝑔,𝑥,𝑦

Detailed syntax breakdown of Definition df-slt
StepHypRef Expression
1 cslt 31038 . 2 class <s
2 vf . . . . . . 7 setvar 𝑓
32cv 1474 . . . . . 6 class 𝑓
4 csur 31037 . . . . . 6 class No
53, 4wcel 1977 . . . . 5 wff 𝑓 No
6 vg . . . . . . 7 setvar 𝑔
76cv 1474 . . . . . 6 class 𝑔
87, 4wcel 1977 . . . . 5 wff 𝑔 No
95, 8wa 383 . . . 4 wff (𝑓 No 𝑔 No )
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1474 . . . . . . . . 9 class 𝑦
1211, 3cfv 5804 . . . . . . . 8 class (𝑓𝑦)
1311, 7cfv 5804 . . . . . . . 8 class (𝑔𝑦)
1412, 13wceq 1475 . . . . . . 7 wff (𝑓𝑦) = (𝑔𝑦)
15 vx . . . . . . . 8 setvar 𝑥
1615cv 1474 . . . . . . 7 class 𝑥
1714, 10, 16wral 2896 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑔𝑦)
1816, 3cfv 5804 . . . . . . 7 class (𝑓𝑥)
1916, 7cfv 5804 . . . . . . 7 class (𝑔𝑥)
20 c1o 7440 . . . . . . . . 9 class 1𝑜
21 c0 3874 . . . . . . . . 9 class
2220, 21cop 4131 . . . . . . . 8 class ⟨1𝑜, ∅⟩
23 c2o 7441 . . . . . . . . 9 class 2𝑜
2420, 23cop 4131 . . . . . . . 8 class ⟨1𝑜, 2𝑜
2521, 23cop 4131 . . . . . . . 8 class ⟨∅, 2𝑜
2622, 24, 25ctp 4129 . . . . . . 7 class {⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}
2718, 19, 26wbr 4583 . . . . . 6 wff (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)
2817, 27wa 383 . . . . 5 wff (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥))
29 con0 5640 . . . . 5 class On
3028, 15, 29wrex 2897 . . . 4 wff 𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥))
319, 30wa 383 . . 3 wff ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))
3231, 2, 6copab 4642 . 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
331, 32wceq 1475 1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
 Colors of variables: wff setvar class This definition is referenced by:  sltval  31044  sltso  31068
 Copyright terms: Public domain W3C validator