Metamath Proof Explorer

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 e. NN0_s
2 n0cut2 
 |-  ( 1s e. NN0_s -> ( 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