Theorem 1p1e2s

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

	Ref	Expression
Assertion	1p1e2s	⊢ ( 1s +s 1s ) = 2s

Proof

Step	Hyp	Ref	Expression
1		0sno	⊢ 0s ∈ No
2	1	elexi	⊢ 0s ∈ V
3		oveq1	⊢ ( 𝑦 = 0s → ( 𝑦 +s 1s ) = ( 0s +s 1s ) )
4	3	eqeq2d	⊢ ( 𝑦 = 0s → ( 𝑥 = ( 𝑦 +s 1s ) ↔ 𝑥 = ( 0s +s 1s ) ) )
5	2 4	rexsn	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) ↔ 𝑥 = ( 0s +s 1s ) )
6		1sno	⊢ 1s ∈ No
7		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
8	6 7	ax-mp	⊢ ( 0s +s 1s ) = 1s
9	8	eqeq2i	⊢ ( 𝑥 = ( 0s +s 1s ) ↔ 𝑥 = 1s )
10	5 9	bitri	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) ↔ 𝑥 = 1s )
11	10	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } = { 𝑥 ∣ 𝑥 = 1s }
12		df-sn	⊢ { 1s } = { 𝑥 ∣ 𝑥 = 1s }
13	11 12	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } = { 1s }
14		oveq2	⊢ ( 𝑦 = 0s → ( 1s +s 𝑦 ) = ( 1s +s 0s ) )
15	14	eqeq2d	⊢ ( 𝑦 = 0s → ( 𝑥 = ( 1s +s 𝑦 ) ↔ 𝑥 = ( 1s +s 0s ) ) )
16	2 15	rexsn	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) ↔ 𝑥 = ( 1s +s 0s ) )
17		addsrid	⊢ ( 1s ∈ No → ( 1s +s 0s ) = 1s )
18	6 17	ax-mp	⊢ ( 1s +s 0s ) = 1s
19	18	eqeq2i	⊢ ( 𝑥 = ( 1s +s 0s ) ↔ 𝑥 = 1s )
20	16 19	bitri	⊢ ( ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) ↔ 𝑥 = 1s )
21	20	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } = { 𝑥 ∣ 𝑥 = 1s }
22	21 12	eqtr4i	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } = { 1s }
23	13 22	uneq12i	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } ) = ( { 1s } ∪ { 1s } )
24		unidm	⊢ ( { 1s } ∪ { 1s } ) = { 1s }
25	23 24	eqtri	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } ) = { 1s }
26		rex0	⊢ ¬ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s )
27	26	abf	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s ) } = ∅
28		rex0	⊢ ¬ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 )
29	28	abf	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 ) } = ∅
30	27 29	uneq12i	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 ) } ) = ( ∅ ∪ ∅ )
31		unidm	⊢ ( ∅ ∪ ∅ ) = ∅
32	30 31	eqtri	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 ) } ) = ∅
33	25 32	oveq12i	⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 ) } ) ) = ( { 1s } |s ∅ )
34		snelpwi	⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
35	1 34	ax-mp	⊢ { 0s } ∈ 𝒫 No
36		nulssgt	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
37	35 36	ax-mp	⊢ { 0s } <<s ∅
38	37	a1i	⊢ ( ⊤ → { 0s } <<s ∅ )
39		df-1s	⊢ 1s = ( { 0s } |s ∅ )
40	39	a1i	⊢ ( ⊤ → 1s = ( { 0s } |s ∅ ) )
41	38 38 40 40	addsunif	⊢ ( ⊤ → ( 1s +s 1s ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 ) } ) ) )
42	41	mptru	⊢ ( 1s +s 1s ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ { 0s } 𝑥 = ( 1s +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 1s ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 1s +s 𝑦 ) } ) )
43		df-2s	⊢ 2s = ( { 1s } |s ∅ )
44	33 42 43	3eqtr4i	⊢ ( 1s +s 1s ) = 2s