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	Could not format assertion : No typesetting found for |- ( A e. No -> { x e. On_s | x

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		sltonold	Could not format ( A e. No -> { x e. On_s | x { x e. On_s | x
3	1 2	ssexd	Could not format ( A e. No -> { x e. On_s | x { x e. On_s | x