Theorem nnn0sd

Description: A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Hypothesis	nnn0sd.1	|- ( ph -> A e. NN_s )
Assertion	nnn0sd	|- ( ph -> A e. NN0_s )

Proof

Step	Hyp	Ref	Expression
1		nnn0sd.1	|- ( ph -> A e. NN_s )
2		nnssn0s	|- NN_s C_ NN0_s
3	2 1	sselid	|- ( ph -> A e. NN0_s )