Metamath Proof Explorer


Theorem 0n0s

Description: Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025)

Ref Expression
Assertion 0n0s
|- 0s e. NN0_s

Proof

Step Hyp Ref Expression
1 df-n0s
 |-  NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om )
2 1 a1i
 |-  ( T. -> NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) )
3 0sno
 |-  0s e. No
4 3 a1i
 |-  ( T. -> 0s e. No )
5 2 4 noseq0
 |-  ( T. -> 0s e. NN0_s )
6 5 mptru
 |-  0s e. NN0_s