Metamath Proof Explorer

Theorem 1ne0s

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

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

Proof

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