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\in {On}_s\to A=L\left(A\right){|}_s\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		onsno	$$⊢A\in {On}_s\to A\in \mathrm{No}$$
2		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
3	1 2	syl	$$⊢A\in {On}_s\to L\left(A\right){|}_{s}R\left(A\right)=A$$
4		elons	$$⊢A\in {On}_s\leftrightarrow \left(A\in \mathrm{No}\wedge R\left(A\right)=\varnothing \right)$$
5	4	simprbi	$$⊢A\in {On}_s\to R\left(A\right)=\varnothing$$
6	5	oveq2d	$$⊢A\in {On}_s\to L\left(A\right){|}_{s}R\left(A\right)=L\left(A\right){|}_s\varnothing$$
7	3 6	eqtr3d	$$⊢A\in {On}_s\to A=L\left(A\right){|}_s\varnothing$$