Theorem eln0s2

Description: A non-negative surreal integer is a surreal ordinal with a finite birthday. (Contributed by Scott Fenton, 27-Feb-2026)

	Ref	Expression
Assertion	eln0s2	|- ( A e. NN0_s <-> ( A e. On_s /\ ( bday ` A ) e. _om ) )

Proof

Step	Hyp	Ref	Expression
1		n0on	|- ( A e. NN0_s -> A e. On_s )
2		n0bday	|- ( A e. NN0_s -> ( bday ` A ) e. _om )
3	1 2	jca	|- ( A e. NN0_s -> ( A e. On_s /\ ( bday ` A ) e. _om ) )
4		onsfi	|- ( ( A e. On_s /\ ( bday ` A ) e. _om ) -> A e. NN0_s )
5	3 4	impbii	|- ( A e. NN0_s <-> ( A e. On_s /\ ( bday ` A ) e. _om ) )