Theorem sltonex

Description: The class of ordinals less than any particular surreal is a set. Theorem 14 of Conway p. 27. (Contributed by Scott Fenton, 22-Mar-2025)

	Ref	Expression
Assertion	sltonex	|- ( A e. No -> { x e. On_s | x

Proof

Step	Hyp	Ref	Expression
1		fvexd	|- ( A e. No -> ( _Old ` ( bday ` A ) ) e. _V )
2		sltonold	|- ( A e. No -> { x e. On_s | x
3	1 2	ssexd	|- ( A e. No -> { x e. On_s | x