Theorem onswe

Description: Surreal less-than well-orders the surreal ordinals. Part of Theorem 15 of Conway p. 28. (Contributed by Scott Fenton, 6-Nov-2025)

	Ref	Expression
Assertion	onswe	⊢ <s We Ons

Proof

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