Theorem onsse

Description: Surreal less-than is set-like over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025)

	Ref	Expression
Assertion	onsse	⊢ <s Se Ons

Proof

Step	Hyp	Ref	Expression
1		epse	⊢ E Se On
2		oniso	⊢ ( bday ↾ Ons ) Isom <s , E ( Ons , On )
3		isose	⊢ ( ( bday ↾ Ons ) Isom <s , E ( Ons , On ) → ( <s Se Ons ↔ E Se On ) )
4	2 3	ax-mp	⊢ ( <s Se Ons ↔ E Se On )
5	1 4	mpbir	⊢ <s Se Ons