Metamath Proof Explorer

Theorem 0sno

Description: Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion 0sno 
|- 0s e. No

Proof

Step Hyp Ref Expression
1 df-0s 
 |-  0s = ( (/) |s (/) )
2 0elpw 
 |-  (/) e. ~P No
3 nulssgt 
 |-  ( (/) e. ~P No -> (/) <
4 2 3 ax-mp 
 |-  (/) <
5 scutcl 
 |-  ( (/) < ( (/) |s (/) ) e. No )
6 4 5 ax-mp 
 |-  ( (/) |s (/) ) e. No
7 1 6 eqeltri 
 |-  0s e. No