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	⊢ ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		fvexd	⊢ ( 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) ∈ V )
2		ltonold	⊢ ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
3	1 2	ssexd	⊢ ( 𝐴 ∈ No → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } ∈ V )