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 32172
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 32169 . 2 class <s
2 vf . . . . . . 7 setvar 𝑓
32cv 1651 . . . . . 6 class 𝑓
4 csur 32168 . . . . . 6 class No
53, 4wcel 2155 . . . . 5 wff 𝑓 No
6 vg . . . . . . 7 setvar 𝑔
76cv 1651 . . . . . 6 class 𝑔
87, 4wcel 2155 . . . . 5 wff 𝑔 No
95, 8wa 384 . . . 4 wff (𝑓 No 𝑔 No )
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1651 . . . . . . . . 9 class 𝑦
1211, 3cfv 6067 . . . . . . . 8 class (𝑓𝑦)
1311, 7cfv 6067 . . . . . . . 8 class (𝑔𝑦)
1412, 13wceq 1652 . . . . . . 7 wff (𝑓𝑦) = (𝑔𝑦)
15 vx . . . . . . . 8 setvar 𝑥
1615cv 1651 . . . . . . 7 class 𝑥
1714, 10, 16wral 3054 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑔𝑦)
1816, 3cfv 6067 . . . . . . 7 class (𝑓𝑥)
1916, 7cfv 6067 . . . . . . 7 class (𝑔𝑥)
20 c1o 7756 . . . . . . . . 9 class 1𝑜
21 c0 4078 . . . . . . . . 9 class
2220, 21cop 4339 . . . . . . . 8 class ⟨1𝑜, ∅⟩
23 c2o 7757 . . . . . . . . 9 class 2𝑜
2420, 23cop 4339 . . . . . . . 8 class ⟨1𝑜, 2𝑜
2521, 23cop 4339 . . . . . . . 8 class ⟨∅, 2𝑜
2622, 24, 25ctp 4337 . . . . . . 7 class {⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}
2718, 19, 26wbr 4808 . . . . . 6 wff (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)
2817, 27wa 384 . . . . 5 wff (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥))
29 con0 5907 . . . . 5 class On
3028, 15, 29wrex 3055 . . . 4 wff 𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥))
319, 30wa 384 . . 3 wff ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))
3231, 2, 6copab 4870 . 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
331, 32wceq 1652 1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  sltval  32175  sltso  32202
  Copyright terms: Public domain W3C validator