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\mathrm{We}{On}_s$$

Proof

Step	Hyp	Ref	Expression
1		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
2		oniso	$$⊢\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right){Isom}_{{<}_s,\mathrm{E}}\left({On}_s,\mathrm{On}\right)$$
3		isowe	$$⊢\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right){Isom}_{{<}_s,\mathrm{E}}\left({On}_s,\mathrm{On}\right)\to \left({<}_s\mathrm{We}{On}_s\leftrightarrow \mathrm{E}\mathrm{We}\mathrm{On}\right)$$
4	2 3	ax-mp	$$⊢{<}_s\mathrm{We}{On}_s\leftrightarrow \mathrm{E}\mathrm{We}\mathrm{On}$$
5	1 4	mpbir	$$⊢{<}_s\mathrm{We}{On}_s$$