Theorem onssno

Description: The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025)

	Ref	Expression
Assertion	onssno	⊢ Ons ⊆ No

Proof

Step	Hyp	Ref	Expression
1		df-ons	⊢ Ons = { 𝑥 ∈ No ∣ ( R ‘ 𝑥 ) = ∅ }
2		ssrab2	⊢ { 𝑥 ∈ No ∣ ( R ‘ 𝑥 ) = ∅ } ⊆ No
3	1 2	eqsstri	⊢ Ons ⊆ No