Theorem onleft

Description: The left set of a surreal ordinal is the same as its old set. (Contributed by Scott Fenton, 6-Nov-2025)

	Ref	Expression
Assertion	onleft	$$⊢A\in {On}_s\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)=L\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elons	$$⊢A\in {On}_s\leftrightarrow \left(A\in \mathrm{No}\wedge R\left(A\right)=\varnothing \right)$$
2	1	simprbi	$$⊢A\in {On}_s\to R\left(A\right)=\varnothing$$
3	2	uneq2d	$$⊢A\in {On}_s\to L\left(A\right)\cup R\left(A\right)=L\left(A\right)\cup \varnothing$$
4		lrold	$$⊢L\left(A\right)\cup R\left(A\right)=\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
5		un0	$$⊢L\left(A\right)\cup \varnothing =L\left(A\right)$$
6	3 4 5	3eqtr3g	$$⊢A\in {On}_s\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)=L\left(A\right)$$