Theorem scutcut

Description: Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	scutcut	$$⊢A{\ll }_{s}B\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		scutval	$$⊢A{\ll }_{s}B\to A{|}_{s}B=\left(\iota x\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}|\mathrm{bday}\left(x\right)=\bigcap \mathrm{bday}\left[\left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\right]\right)$$
2		conway	$$⊢A{\ll }_{s}B\to \exists !x\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\mathrm{bday}\left(x\right)=\bigcap \mathrm{bday}\left[\left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\right]$$
3		riotacl	$$⊢\exists !x\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\mathrm{bday}\left(x\right)=\bigcap \mathrm{bday}\left[\left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\right]\to \left(\iota x\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}|\mathrm{bday}\left(x\right)=\bigcap \mathrm{bday}\left[\left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\right]\right)\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}$$
4	2 3	syl	$$⊢A{\ll }_{s}B\to \left(\iota x\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}|\mathrm{bday}\left(x\right)=\bigcap \mathrm{bday}\left[\left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\right]\right)\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}$$
5	1 4	eqeltrd	$$⊢A{\ll }_{s}B\to A{|}_{s}B\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}$$
6		sneq	$$⊢y=A{|}_{s}B\to \left\{y\right\}=\left\{A{|}_{s}B\right\}$$
7	6	breq2d	$$⊢y=A{|}_{s}B\to \left(A{\ll }_s\left\{y\right\}\leftrightarrow A{\ll }_s\left\{A{|}_{s}B\right\}\right)$$
8	6	breq1d	$$⊢y=A{|}_{s}B\to \left(\left\{y\right\}{\ll }_{s}B\leftrightarrow \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
9	7 8	anbi12d	$$⊢y=A{|}_{s}B\to \left(\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\leftrightarrow \left(A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)\right)$$
10	9	elrab	$$⊢A{|}_{s}B\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\leftrightarrow \left(A{|}_{s}B\in \mathrm{No}\wedge \left(A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)\right)$$
11		3anass	$$⊢\left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)\leftrightarrow \left(A{|}_{s}B\in \mathrm{No}\wedge \left(A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)\right)$$
12	10 11	bitr4i	$$⊢A{|}_{s}B\in \left\{y\in \mathrm{No}|\left(A{\ll }_s\left\{y\right\}\wedge \left\{y\right\}{\ll }_{s}B\right)\right\}\leftrightarrow \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
13	5 12	sylib	$$⊢A{\ll }_{s}B\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$