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		1n0s	⊢ 1s ∈ ℕ0s
2		n0cut2	⊢ ( 1s ∈ ℕ0s → ( 1s +s 1s ) = ( { 1s } |s ∅ ) )
3	1 2	ax-mp	⊢ ( 1s +s 1s ) = ( { 1s } |s ∅ )
4		df-2s	⊢ 2s = ( { 1s } |s ∅ )
5	3 4	eqtr4i	⊢ ( 1s +s 1s ) = 2s