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 0sno 
 |-  0s e. No
2 1 elexi 
 |-  0s e. _V
3 oveq1 
 |-  ( y = 0s -> ( y +s 1s ) = ( 0s +s 1s ) )
4 3 eqeq2d 
 |-  ( y = 0s -> ( x = ( y +s 1s ) <-> x = ( 0s +s 1s ) ) )
5 2 4 rexsn 
 |-  ( E. y e. { 0s } x = ( y +s 1s ) <-> x = ( 0s +s 1s ) )
6 1sno 
 |-  1s e. No
7 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
8 6 7 ax-mp 
 |-  ( 0s +s 1s ) = 1s
9 8 eqeq2i 
 |-  ( x = ( 0s +s 1s ) <-> x = 1s )
10 5 9 bitri 
 |-  ( E. y e. { 0s } x = ( y +s 1s ) <-> x = 1s )
11 10 abbii 
 |-  { x | E. y e. { 0s } x = ( y +s 1s ) } = { x | x = 1s }
12 df-sn 
 |-  { 1s } = { x | x = 1s }
13 11 12 eqtr4i 
 |-  { x | E. y e. { 0s } x = ( y +s 1s ) } = { 1s }
14 oveq2 
 |-  ( y = 0s -> ( 1s +s y ) = ( 1s +s 0s ) )
15 14 eqeq2d 
 |-  ( y = 0s -> ( x = ( 1s +s y ) <-> x = ( 1s +s 0s ) ) )
16 2 15 rexsn 
 |-  ( E. y e. { 0s } x = ( 1s +s y ) <-> x = ( 1s +s 0s ) )
17 addsrid 
 |-  ( 1s e. No -> ( 1s +s 0s ) = 1s )
18 6 17 ax-mp 
 |-  ( 1s +s 0s ) = 1s
19 18 eqeq2i 
 |-  ( x = ( 1s +s 0s ) <-> x = 1s )
20 16 19 bitri 
 |-  ( E. y e. { 0s } x = ( 1s +s y ) <-> x = 1s )
21 20 abbii 
 |-  { x | E. y e. { 0s } x = ( 1s +s y ) } = { x | x = 1s }
22 21 12 eqtr4i 
 |-  { x | E. y e. { 0s } x = ( 1s +s y ) } = { 1s }
23 13 22 uneq12i 
 |-  ( { x | E. y e. { 0s } x = ( y +s 1s ) } u. { x | E. y e. { 0s } x = ( 1s +s y ) } ) = ( { 1s } u. { 1s } )
24 unidm 
 |-  ( { 1s } u. { 1s } ) = { 1s }
25 23 24 eqtri 
 |-  ( { x | E. y e. { 0s } x = ( y +s 1s ) } u. { x | E. y e. { 0s } x = ( 1s +s y ) } ) = { 1s }
26 rex0 
 |-  -. E. y e. (/) x = ( y +s 1s )
27 26 abf 
 |-  { x | E. y e. (/) x = ( y +s 1s ) } = (/)
28 rex0 
 |-  -. E. y e. (/) x = ( 1s +s y )
29 28 abf 
 |-  { x | E. y e. (/) x = ( 1s +s y ) } = (/)
30 27 29 uneq12i 
 |-  ( { x | E. y e. (/) x = ( y +s 1s ) } u. { x | E. y e. (/) x = ( 1s +s y ) } ) = ( (/) u. (/) )
31 unidm 
 |-  ( (/) u. (/) ) = (/)
32 30 31 eqtri 
 |-  ( { x | E. y e. (/) x = ( y +s 1s ) } u. { x | E. y e. (/) x = ( 1s +s y ) } ) = (/)
33 25 32 oveq12i 
 |-  ( ( { x | E. y e. { 0s } x = ( y +s 1s ) } u. { x | E. y e. { 0s } x = ( 1s +s y ) } ) |s ( { x | E. y e. (/) x = ( y +s 1s ) } u. { x | E. y e. (/) x = ( 1s +s y ) } ) ) = ( { 1s } |s (/) )
34 snelpwi 
 |-  ( 0s e. No -> { 0s } e. ~P No )
35 1 34 ax-mp 
 |-  { 0s } e. ~P No
36 nulssgt 
 |-  ( { 0s } e. ~P No -> { 0s } <
37 35 36 ax-mp 
 |-  { 0s } <
38 37 a1i 
 |-  ( T. -> { 0s } <
39 df-1s 
 |-  1s = ( { 0s } |s (/) )
40 39 a1i 
 |-  ( T. -> 1s = ( { 0s } |s (/) ) )
41 38 38 40 40 addsunif 
 |-  ( T. -> ( 1s +s 1s ) = ( ( { x | E. y e. { 0s } x = ( y +s 1s ) } u. { x | E. y e. { 0s } x = ( 1s +s y ) } ) |s ( { x | E. y e. (/) x = ( y +s 1s ) } u. { x | E. y e. (/) x = ( 1s +s y ) } ) ) )
42 41 mptru 
 |-  ( 1s +s 1s ) = ( ( { x | E. y e. { 0s } x = ( y +s 1s ) } u. { x | E. y e. { 0s } x = ( 1s +s y ) } ) |s ( { x | E. y e. (/) x = ( y +s 1s ) } u. { x | E. y e. (/) x = ( 1s +s y ) } ) )
43 df-2s 
 |-  2s = ( { 1s } |s (/) )
44 33 42 43 3eqtr4i 
 |-  ( 1s +s 1s ) = 2s