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 32024
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 32021 . 2 class <s
2 vf . . . . . . 7 setvar 𝑓
32cv 1595 . . . . . 6 class 𝑓
4 csur 32020 . . . . . 6 class No
53, 4wcel 2103 . . . . 5 wff 𝑓 No
6 vg . . . . . . 7 setvar 𝑔
76cv 1595 . . . . . 6 class 𝑔
87, 4wcel 2103 . . . . 5 wff 𝑔 No
95, 8wa 383 . . . 4 wff (𝑓 No 𝑔 No )
10 vy . . . . . . . . . 10 setvar 𝑦
1110cv 1595 . . . . . . . . 9 class 𝑦
1211, 3cfv 6001 . . . . . . . 8 class (𝑓𝑦)
1311, 7cfv 6001 . . . . . . . 8 class (𝑔𝑦)
1412, 13wceq 1596 . . . . . . 7 wff (𝑓𝑦) = (𝑔𝑦)
15 vx . . . . . . . 8 setvar 𝑥
1615cv 1595 . . . . . . 7 class 𝑥
1714, 10, 16wral 3014 . . . . . 6 wff 𝑦𝑥 (𝑓𝑦) = (𝑔𝑦)
1816, 3cfv 6001 . . . . . . 7 class (𝑓𝑥)
1916, 7cfv 6001 . . . . . . 7 class (𝑔𝑥)
20 c1o 7673 . . . . . . . . 9 class 1𝑜
21 c0 4023 . . . . . . . . 9 class
2220, 21cop 4291 . . . . . . . 8 class ⟨1𝑜, ∅⟩
23 c2o 7674 . . . . . . . . 9 class 2𝑜
2420, 23cop 4291 . . . . . . . 8 class ⟨1𝑜, 2𝑜
2521, 23cop 4291 . . . . . . . 8 class ⟨∅, 2𝑜
2622, 24, 25ctp 4289 . . . . . . 7 class {⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}
2718, 19, 26wbr 4760 . . . . . 6 wff (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)
2817, 27wa 383 . . . . 5 wff (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥))
29 con0 5836 . . . . 5 class On
3028, 15, 29wrex 3015 . . . 4 wff 𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥))
319, 30wa 383 . . 3 wff ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))
3231, 2, 6copab 4820 . 2 class {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
331, 32wceq 1596 1 wff <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
Colors of variables: wff setvar class
This definition is referenced by:  sltval  32027  sltso  32054
  Copyright terms: Public domain W3C validator