Theorem onsleft

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	onsleft	|- ( A e. On_s -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )

Proof

Step	Hyp	Ref	Expression
1		elons	|- ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) )
2	1	simprbi	|- ( A e. On_s -> ( _Right ` A ) = (/) )
3	2	uneq2d	|- ( A e. On_s -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( ( _Left ` A ) u. (/) ) )
4		lrold	|- ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) )
5		un0	|- ( ( _Left ` A ) u. (/) ) = ( _Left ` A )
6	3 4 5	3eqtr3g	|- ( A e. On_s -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )