Theorem onscutleft

Description: A surreal ordinal is equal to the cut of its left set and the empty set. (Contributed by Scott Fenton, 29-Mar-2025)

	Ref	Expression
Assertion	onscutleft	|- ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )

Proof

Step	Hyp	Ref	Expression
1		onsno	|- ( A e. On_s -> A e. No )
2		lrcut	|- ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
3	1 2	syl	|- ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
4		elons	|- ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) )
5	4	simprbi	|- ( A e. On_s -> ( _Right ` A ) = (/) )
6	5	oveq2d	|- ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` A ) |s (/) ) )
7	3 6	eqtr3d	|- ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )