Theorem negcut2

Description: The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Assertion	negcut2	$$⊢A\in \mathrm{No}\to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$

Proof

Step	Hyp	Ref	Expression
1		negcut	$$⊢A\in \mathrm{No}\to \left({+}_s\left(A\right)\in \mathrm{No}\wedge {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}\wedge \left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)$$
2	1	simp2d	$$⊢A\in \mathrm{No}\to {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}$$
3	1	simp3d	$$⊢A\in \mathrm{No}\to \left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]$$
4		fvex	$$⊢{+}_s\left(A\right)\in \mathrm{V}$$
5	4	snnz	$$⊢\left\{{+}_s\left(A\right)\right\}\ne \varnothing$$
6		sltstr	$$⊢\left({+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}\wedge \left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\wedge \left\{{+}_s\left(A\right)\right\}\ne \varnothing \right)\to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$
7	5 6	mp3an3	$$⊢\left({+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}\wedge \left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)\to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$
8	2 3 7	syl2anc	$$⊢A\in \mathrm{No}\to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$