Metamath Proof Explorer

Theorem 1sne0s

Description: Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025)

Ref Expression
Assertion 1sne0s 
|- 1s =/= 0s

Proof

Step Hyp Ref Expression
1 0slt1s 
 |-  0s
2 sgt0ne0 
 |-  ( 0s  1s =/= 0s )
3 1 2 ax-mp 
 |-  1s =/= 0s