Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sltso Structured version   Visualization version   GIF version

Theorem sltso 33289
 Description: Surreal less than totally orders the surreals. Alling's axiom (O). (Contributed by Scott Fenton, 9-Jun-2011.)
Assertion
Ref Expression
sltso <s Or No

Proof of Theorem sltso
Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sltsolem1 33288 . 2 {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅})
2 df-no 33258 . 2 No = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1o, 2o}}
3 df-slt 33259 . 2 <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔𝑥)))}
4 nosgnn0 33273 . 2 ¬ ∅ ∈ {1o, 2o}
51, 2, 3, 4soseq 33204 1 <s Or No
 Colors of variables: wff setvar class Syntax hints:  ∅c0 4246  {cpr 4530  {ctp 4532  ⟨cop 4534   Or wor 5441  1oc1o 8082  2oc2o 8083   No csur 33255
 Copyright terms: Public domain W3C validator