Theorem 1n0s

Description: Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		1sno	|- 1s e. No
2		addslid	|- ( 1s e. No -> ( 0s +s 1s ) = 1s )
3	1 2	ax-mp	|- ( 0s +s 1s ) = 1s
4		0n0s	|- 0s e. NN0_s
5		peano2n0s	|- ( 0s e. NN0_s -> ( 0s +s 1s ) e. NN0_s )
6	4 5	ax-mp	|- ( 0s +s 1s ) e. NN0_s
7	3 6	eqeltrri	|- 1s e. NN0_s