Theorem 1p1e2s

Description: One plus one is two. Surreal version. (Contributed by Scott Fenton, 27-May-2025)

	Ref	Expression
Assertion	1p1e2s	Could not format assertion : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2	1	elexi	$$⊢0_s\in \mathrm{V}$$
3		oveq1	$$⊢y=0_s\to y{+}_s{1}_s=0_s{+}_s{1}_s$$
4	3	eqeq2d	$$⊢y=0_s\to \left(x=y{+}_s{1}_s\leftrightarrow x=0_s{+}_s{1}_s\right)$$
5	2 4	rexsn	$$⊢\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\leftrightarrow x=0_s{+}_s{1}_s$$
6		1sno	$$⊢1_s\in \mathrm{No}$$
7		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
8	6 7	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
9	8	eqeq2i	$$⊢x=0_s{+}_s{1}_s\leftrightarrow x=1_s$$
10	5 9	bitri	$$⊢\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\leftrightarrow x=1_s$$
11	10	abbii	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}=\left\{x|x=1_s\right\}$$
12		df-sn	$$⊢\left\{1_s\right\}=\left\{x|x=1_s\right\}$$
13	11 12	eqtr4i	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}=\left\{1_s\right\}$$
14		oveq2	$$⊢y=0_s\to 1_s{+}_{s}y=1_s{+}_s{0}_s$$
15	14	eqeq2d	$$⊢y=0_s\to \left(x=1_s{+}_{s}y\leftrightarrow x=1_s{+}_s{0}_s\right)$$
16	2 15	rexsn	$$⊢\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\leftrightarrow x=1_s{+}_s{0}_s$$
17		addsrid	$$⊢1_s\in \mathrm{No}\to 1_s{+}_s{0}_s=1_s$$
18	6 17	ax-mp	$$⊢1_s{+}_s{0}_s=1_s$$
19	18	eqeq2i	$$⊢x=1_s{+}_s{0}_s\leftrightarrow x=1_s$$
20	16 19	bitri	$$⊢\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\leftrightarrow x=1_s$$
21	20	abbii	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}=\left\{x|x=1_s\right\}$$
22	21 12	eqtr4i	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}=\left\{1_s\right\}$$
23	13 22	uneq12i	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}=\left\{1_s\right\}\cup \left\{1_s\right\}$$
24		unidm	$$⊢\left\{1_s\right\}\cup \left\{1_s\right\}=\left\{1_s\right\}$$
25	23 24	eqtri	$$⊢\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}=\left\{1_s\right\}$$
26		rex0	$$⊢\neg \exists y\in \varnothing x=y{+}_s{1}_s$$
27	26	abf	$$⊢\left\{x|\exists y\in \varnothing x=y{+}_s{1}_s\right\}=\varnothing$$
28		rex0	$$⊢\neg \exists y\in \varnothing x=1_s{+}_{s}y$$
29	28	abf	$$⊢\left\{x|\exists y\in \varnothing x=1_s{+}_{s}y\right\}=\varnothing$$
30	27 29	uneq12i	$$⊢\left\{x|\exists y\in \varnothing x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \varnothing x=1_s{+}_{s}y\right\}=\varnothing \cup \varnothing$$
31		unidm	$$⊢\varnothing \cup \varnothing =\varnothing$$
32	30 31	eqtri	$$⊢\left\{x|\exists y\in \varnothing x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \varnothing x=1_s{+}_{s}y\right\}=\varnothing$$
33	25 32	oveq12i	$$⊢\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \varnothing x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \varnothing x=1_s{+}_{s}y\right\}\right)=\left\{1_s\right\}{|}_s\varnothing$$
34		snelpwi	$$⊢0_s\in \mathrm{No}\to \left\{0_s\right\}\in 𝒫\mathrm{No}$$
35	1 34	ax-mp	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
36		nulssgt	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
37	35 36	ax-mp	$$⊢\left\{0_s\right\}{\ll }_s\varnothing$$
38	37	a1i	$$⊢\top \to \left\{0_s\right\}{\ll }_s\varnothing$$
39		df-1s	$$⊢1_s=\left\{0_s\right\}{|}_s\varnothing$$
40	39	a1i	$$⊢\top \to 1_s=\left\{0_s\right\}{|}_s\varnothing$$
41	38 38 40 40	addsunif	$$⊢\top \to 1_s{+}_s{1}_s=\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \varnothing x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \varnothing x=1_s{+}_{s}y\right\}\right)$$
42	41	mptru	$$⊢1_s{+}_s{1}_s=\left(\left\{x|\exists y\in \left\{0_s\right\}x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \left\{0_s\right\}x=1_s{+}_{s}y\right\}\right){|}_s\left(\left\{x|\exists y\in \varnothing x=y{+}_s{1}_s\right\}\cup \left\{x|\exists y\in \varnothing x=1_s{+}_{s}y\right\}\right)$$
43		df-2s	Could not format 2s = ( { 1s } |s (/) ) : No typesetting found for |- 2s = ( { 1s } |s (/) ) with typecode |-
44	33 42 43	3eqtr4i	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-