Theorem neg1s

Description: An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025)

	Ref	Expression
Assertion	neg1s	$$⊢{+}_s\left(1_s\right)=\varnothing {|}_s\left\{0_s\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1no	$$⊢1_s\in \mathrm{No}$$
2		negsval	$$⊢1_s\in \mathrm{No}\to {+}_s\left(1_s\right)={+}_s\left[R\left(1_s\right)\right]{|}_s{+}_s\left[L\left(1_s\right)\right]$$
3	1 2	ax-mp	$$⊢{+}_s\left(1_s\right)={+}_s\left[R\left(1_s\right)\right]{|}_s{+}_s\left[L\left(1_s\right)\right]$$
4		right1s	$$⊢R\left(1_s\right)=\varnothing$$
5	4	imaeq2i	$$⊢{+}_s\left[R\left(1_s\right)\right]={+}_s\left[\varnothing \right]$$
6		ima0	$$⊢{+}_s\left[\varnothing \right]=\varnothing$$
7	5 6	eqtri	$$⊢{+}_s\left[R\left(1_s\right)\right]=\varnothing$$
8		left1s	$$⊢L\left(1_s\right)=\left\{0_s\right\}$$
9	8	imaeq2i	$$⊢{+}_s\left[L\left(1_s\right)\right]={+}_s\left[\left\{0_s\right\}\right]$$
10		negsfn	$$⊢{+}_{s}Fn\mathrm{No}$$
11		0no	$$⊢0_s\in \mathrm{No}$$
12		fnimapr	$$⊢\left({+}_{s}Fn\mathrm{No}\wedge 0_s\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to {+}_s\left[\left\{0_s,0_s\right\}\right]=\left\{{+}_s\left(0_s\right),{+}_s\left(0_s\right)\right\}$$
13	10 11 11 12	mp3an	$$⊢{+}_s\left[\left\{0_s,0_s\right\}\right]=\left\{{+}_s\left(0_s\right),{+}_s\left(0_s\right)\right\}$$
14		neg0s	$$⊢{+}_s\left(0_s\right)=0_s$$
15	14 14	preq12i	$$⊢\left\{{+}_s\left(0_s\right),{+}_s\left(0_s\right)\right\}=\left\{0_s,0_s\right\}$$
16	13 15	eqtri	$$⊢{+}_s\left[\left\{0_s,0_s\right\}\right]=\left\{0_s,0_s\right\}$$
17		dfsn2	$$⊢\left\{0_s\right\}=\left\{0_s,0_s\right\}$$
18	17	imaeq2i	$$⊢{+}_s\left[\left\{0_s\right\}\right]={+}_s\left[\left\{0_s,0_s\right\}\right]$$
19	16 18 17	3eqtr4i	$$⊢{+}_s\left[\left\{0_s\right\}\right]=\left\{0_s\right\}$$
20	9 19	eqtri	$$⊢{+}_s\left[L\left(1_s\right)\right]=\left\{0_s\right\}$$
21	7 20	oveq12i	$$⊢{+}_s\left[R\left(1_s\right)\right]{|}_s{+}_s\left[L\left(1_s\right)\right]=\varnothing {|}_s\left\{0_s\right\}$$
22	3 21	eqtri	$$⊢{+}_s\left(1_s\right)=\varnothing {|}_s\left\{0_s\right\}$$