Theorem ltonsex

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	ltonsex	$$⊢A\in \mathrm{No}\to \left\{x\in {On}_s|x{<}_{s}A\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fvexd	$$⊢A\in \mathrm{No}\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\in \mathrm{V}$$
2		ltonold	$$⊢A\in \mathrm{No}\to \left\{x\in {On}_s|x{<}_{s}A\right\}\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
3	1 2	ssexd	$$⊢A\in \mathrm{No}\to \left\{x\in {On}_s|x{<}_{s}A\right\}\in \mathrm{V}$$