Theorem negsproplem3

Description: Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
	negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	negsproplem3	$$⊢\phi \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)$$

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\left(\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\to \left({+}_s\left(x\right)\in \mathrm{No}\wedge \left(x{<}_{s}y\to {+}_s\left(y\right){<}_s{+}_s\left(x\right)\right)\right)\right)$$
2		negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
3	1 2	negsproplem2	$$⊢\phi \to {+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]$$
4		scutcut	$$⊢{+}_s\left[R\left(A\right)\right]{\ll }_s{+}_s\left[L\left(A\right)\right]\to \left({+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\in \mathrm{No}\wedge {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}\wedge \left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)$$
5	3 4	syl	$$⊢\phi \to \left({+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\in \mathrm{No}\wedge {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}\wedge \left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)$$
6		negsval	$$⊢A\in \mathrm{No}\to {+}_s\left(A\right)={+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]$$
7	2 6	syl	$$⊢\phi \to {+}_s\left(A\right)={+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]$$
8	7	eleq1d	$$⊢\phi \to \left({+}_s\left(A\right)\in \mathrm{No}\leftrightarrow {+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\in \mathrm{No}\right)$$
9	7	sneqd	$$⊢\phi \to \left\{{+}_s\left(A\right)\right\}=\left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}$$
10	9	breq2d	$$⊢\phi \to \left({+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left(A\right)\right\}\leftrightarrow {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}\right)$$
11	9	breq1d	$$⊢\phi \to \left(\left\{{+}_s\left(A\right)\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\leftrightarrow \left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)$$
12	8 10 11	3anbi123d	$$⊢\phi \to \left(\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)\leftrightarrow \left({+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\in \mathrm{No}\wedge {+}_s\left[R\left(A\right)\right]{\ll }_s\left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}\wedge \left\{{+}_s\left[R\left(A\right)\right]{|}_s{+}_s\left[L\left(A\right)\right]\right\}{\ll }_s{+}_s\left[L\left(A\right)\right]\right)\right)$$
13	5 12	mpbird	$$⊢\phi \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)$$