Theorem n0ssold

Description: The non-negative surreal integers are a subset of the old set of _om . (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Assertion	n0ssold	|- NN0_s C_ ( _Old ` _om )

Proof

Step	Hyp	Ref	Expression
1		n0sbday	|- ( n e. NN0_s -> ( bday ` n ) e. _om )
2		omelon	|- _om e. On
3		n0sno	|- ( n e. NN0_s -> n e. No )
4		oldbday	|- ( ( _om e. On /\ n e. No ) -> ( n e. ( _Old ` _om ) <-> ( bday ` n ) e. _om ) )
5	2 3 4	sylancr	|- ( n e. NN0_s -> ( n e. ( _Old ` _om ) <-> ( bday ` n ) e. _om ) )
6	1 5	mpbird	|- ( n e. NN0_s -> n e. ( _Old ` _om ) )
7	6	ssriv	|- NN0_s C_ ( _Old ` _om )