Theorem 0zs

Description: Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	0zs	|- 0s e. ZZ_s

Proof

Step	Hyp	Ref	Expression
1		1nns	|- 1s e. NN_s
2		1sno	|- 1s e. No
3		subsid	|- ( 1s e. No -> ( 1s -s 1s ) = 0s )
4	2 3	ax-mp	|- ( 1s -s 1s ) = 0s
5	4	eqcomi	|- 0s = ( 1s -s 1s )
6		rspceov	|- ( ( 1s e. NN_s /\ 1s e. NN_s /\ 0s = ( 1s -s 1s ) ) -> E. n e. NN_s E. m e. NN_s 0s = ( n -s m ) )
7	1 1 5 6	mp3an	|- E. n e. NN_s E. m e. NN_s 0s = ( n -s m )
8		elzs	|- ( 0s e. ZZ_s <-> E. n e. NN_s E. m e. NN_s 0s = ( n -s m ) )
9	7 8	mpbir	|- 0s e. ZZ_s