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

Proof

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