Metamath Proof Explorer


Theorem sltso

Description: Less-than totally orders the surreals. Axiom O of Alling p. 184. (Contributed by Scott Fenton, 9-Jun-2011)

Ref Expression
Assertion sltso <sOrNo

Proof

Step Hyp Ref Expression
1 sltsolem1 1𝑜1𝑜2𝑜2𝑜Or1𝑜2𝑜
2 df-no No=f|xOnf:x1𝑜2𝑜
3 df-slt <s=fg|fNogNoxOnyxfy=gyfx1𝑜1𝑜2𝑜2𝑜gx
4 nosgnn0 ¬1𝑜2𝑜
5 1 2 3 4 soseq <sOrNo