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

Theorem sltso 32133
 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 32132 . 2 {⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} Or ({1𝑜, 2𝑜} ∪ {∅})
2 df-no 32102 . 2 No = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶{1𝑜, 2𝑜}}
3 df-slt 32103 . 2 <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 No 𝑔 No ) ∧ ∃𝑥 ∈ On (∀𝑦𝑥 (𝑓𝑦) = (𝑔𝑦) ∧ (𝑓𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝑔𝑥)))}
4 nosgnn0 32117 . 2 ¬ ∅ ∈ {1𝑜, 2𝑜}
51, 2, 3, 4soseq 32060 1 <s Or No
 Colors of variables: wff setvar class Syntax hints:  ∅c0 4058  {cpr 4323  {ctp 4325  ⟨cop 4327   Or wor 5186  1𝑜c1o 7722  2𝑜c2o 7723   No csur 32099
 Copyright terms: Public domain W3C validator