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		1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$
2		n0cut2	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s{+}_s{1}_s=\left\{1_s\right\}{|}_s\varnothing$$
3	1 2	ax-mp	$$⊢1_s{+}_s{1}_s=\left\{1_s\right\}{|}_s\varnothing$$
4		df-2s	Could not format 2s = ( { 1s } |s (/) ) : No typesetting found for |- 2s = ( { 1s } |s (/) ) with typecode |-
5	3 4	eqtr4i	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-