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	⊢ ( 𝐴 ∈ Ons → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elons	⊢ ( 𝐴 ∈ Ons ↔ ( 𝐴 ∈ No ∧ ( R ‘ 𝐴 ) = ∅ ) )
2	1	simprbi	⊢ ( 𝐴 ∈ Ons → ( R ‘ 𝐴 ) = ∅ )
3	2	uneq2d	⊢ ( 𝐴 ∈ Ons → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( ( L ‘ 𝐴 ) ∪ ∅ ) )
4		lrold	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) )
5		un0	⊢ ( ( L ‘ 𝐴 ) ∪ ∅ ) = ( L ‘ 𝐴 )
6	3 4 5	3eqtr3g	⊢ ( 𝐴 ∈ Ons → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )