Theorem lrcut

Description: A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	lrcut	$$⊢X\in \mathrm{No}\to L\left(X\right){|}_{s}R\left(X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
2	1	oneli	$$⊢b\in \mathrm{bday}\left(X\right)\to b\in \mathrm{On}$$
3		madebday	$$⊢\left(b\in \mathrm{On}\wedge y\in \mathrm{No}\right)\to \left(y\in M\left(b\right)\leftrightarrow \mathrm{bday}\left(y\right)\subseteq b\right)$$
4	3	biimprd	$$⊢\left(b\in \mathrm{On}\wedge y\in \mathrm{No}\right)\to \left(\mathrm{bday}\left(y\right)\subseteq b\to y\in M\left(b\right)\right)$$
5	2 4	sylan	$$⊢\left(b\in \mathrm{bday}\left(X\right)\wedge y\in \mathrm{No}\right)\to \left(\mathrm{bday}\left(y\right)\subseteq b\to y\in M\left(b\right)\right)$$
6	5	rgen2	$$⊢\forall b\in \mathrm{bday}\left(X\right)\forall y\in \mathrm{No}\left(\mathrm{bday}\left(y\right)\subseteq b\to y\in M\left(b\right)\right)$$
7		madebdaylemlrcut	$$⊢\left(\forall b\in \mathrm{bday}\left(X\right)\forall y\in \mathrm{No}\left(\mathrm{bday}\left(y\right)\subseteq b\to y\in M\left(b\right)\right)\wedge X\in \mathrm{No}\right)\to L\left(X\right){|}_{s}R\left(X\right)=X$$
8	6 7	mpan	$$⊢X\in \mathrm{No}\to L\left(X\right){|}_{s}R\left(X\right)=X$$