Metamath Proof Explorer

Theorem addsid1

Description: Surreal addition to zero is identity. Part of Theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion addsid1 
|- ( A e. No -> ( A +s 0s ) = A )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( a = b -> ( a +s 0s ) = ( b +s 0s ) )
2 id 
 |-  ( a = b -> a = b )
3 1 2 eqeq12d 
 |-  ( a = b -> ( ( a +s 0s ) = a <-> ( b +s 0s ) = b ) )
4 oveq1 
 |-  ( a = A -> ( a +s 0s ) = ( A +s 0s ) )
5 id 
 |-  ( a = A -> a = A )
6 4 5 eqeq12d 
 |-  ( a = A -> ( ( a +s 0s ) = a <-> ( A +s 0s ) = A ) )
7 0sno 
 |-  0s e. No
8 addsval 
 |-  ( ( a e. No /\ 0s e. No ) -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) )
9 7 8 mpan2 
 |-  ( a e. No -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) )
10 9 adantr 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( a +s 0s ) = ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) )
11 elun1 
 |-  ( y e. ( _L ` a ) -> y e. ( ( _L ` a ) u. ( _R ` a ) ) )
12 simpr 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b )
13 oveq1 
 |-  ( b = y -> ( b +s 0s ) = ( y +s 0s ) )
14 id 
 |-  ( b = y -> b = y )
15 13 14 eqeq12d 
 |-  ( b = y -> ( ( b +s 0s ) = b <-> ( y +s 0s ) = y ) )
16 15 rspcva 
 |-  ( ( y e. ( ( _L ` a ) u. ( _R ` a ) ) /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( y +s 0s ) = y )
17 11 12 16 syl2anr 
 |-  ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( y +s 0s ) = y )
18 17 eqeq2d 
 |-  ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( x = ( y +s 0s ) <-> x = y ) )
19 equcom 
 |-  ( x = y <-> y = x )
20 18 19 bitrdi 
 |-  ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ y e. ( _L ` a ) ) -> ( x = ( y +s 0s ) <-> y = x ) )
21 20 rexbidva 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. y e. ( _L ` a ) x = ( y +s 0s ) <-> E. y e. ( _L ` a ) y = x ) )
22 risset 
 |-  ( x e. ( _L ` a ) <-> E. y e. ( _L ` a ) y = x )
23 21 22 bitr4di 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. y e. ( _L ` a ) x = ( y +s 0s ) <-> x e. ( _L ` a ) ) )
24 23 abbi1dv 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } = ( _L ` a ) )
25 rex0 
 |-  -. E. y e. (/) z = ( a +s y )
26 left0s 
 |-  ( _L ` 0s ) = (/)
27 26 rexeqi 
 |-  ( E. y e. ( _L ` 0s ) z = ( a +s y ) <-> E. y e. (/) z = ( a +s y ) )
28 25 27 mtbir 
 |-  -. E. y e. ( _L ` 0s ) z = ( a +s y )
29 28 abf 
 |-  { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } = (/)
30 29 a1i 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } = (/) )
31 24 30 uneq12d 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) = ( ( _L ` a ) u. (/) ) )
32 un0 
 |-  ( ( _L ` a ) u. (/) ) = ( _L ` a )
33 31 32 eqtrdi 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) = ( _L ` a ) )
34 elun2 
 |-  ( w e. ( _R ` a ) -> w e. ( ( _L ` a ) u. ( _R ` a ) ) )
35 oveq1 
 |-  ( b = w -> ( b +s 0s ) = ( w +s 0s ) )
36 id 
 |-  ( b = w -> b = w )
37 35 36 eqeq12d 
 |-  ( b = w -> ( ( b +s 0s ) = b <-> ( w +s 0s ) = w ) )
38 37 rspcva 
 |-  ( ( w e. ( ( _L ` a ) u. ( _R ` a ) ) /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( w +s 0s ) = w )
39 34 12 38 syl2anr 
 |-  ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( w +s 0s ) = w )
40 39 eqeq2d 
 |-  ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( x = ( w +s 0s ) <-> x = w ) )
41 equcom 
 |-  ( x = w <-> w = x )
42 40 41 bitrdi 
 |-  ( ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) /\ w e. ( _R ` a ) ) -> ( x = ( w +s 0s ) <-> w = x ) )
43 42 rexbidva 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. w e. ( _R ` a ) x = ( w +s 0s ) <-> E. w e. ( _R ` a ) w = x ) )
44 risset 
 |-  ( x e. ( _R ` a ) <-> E. w e. ( _R ` a ) w = x )
45 43 44 bitr4di 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( E. w e. ( _R ` a ) x = ( w +s 0s ) <-> x e. ( _R ` a ) ) )
46 45 abbi1dv 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } = ( _R ` a ) )
47 rex0 
 |-  -. E. w e. (/) z = ( a +s w )
48 right0s 
 |-  ( _R ` 0s ) = (/)
49 48 rexeqi 
 |-  ( E. w e. ( _R ` 0s ) z = ( a +s w ) <-> E. w e. (/) z = ( a +s w ) )
50 47 49 mtbir 
 |-  -. E. w e. ( _R ` 0s ) z = ( a +s w )
51 50 abf 
 |-  { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } = (/)
52 51 a1i 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } = (/) )
53 46 52 uneq12d 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) = ( ( _R ` a ) u. (/) ) )
54 un0 
 |-  ( ( _R ` a ) u. (/) ) = ( _R ` a )
55 53 54 eqtrdi 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) = ( _R ` a ) )
56 33 55 oveq12d 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( ( { x | E. y e. ( _L ` a ) x = ( y +s 0s ) } u. { z | E. y e. ( _L ` 0s ) z = ( a +s y ) } ) |s ( { x | E. w e. ( _R ` a ) x = ( w +s 0s ) } u. { z | E. w e. ( _R ` 0s ) z = ( a +s w ) } ) ) = ( ( _L ` a ) |s ( _R ` a ) ) )
57 lrcut 
 |-  ( a e. No -> ( ( _L ` a ) |s ( _R ` a ) ) = a )
58 57 adantr 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( ( _L ` a ) |s ( _R ` a ) ) = a )
59 10 56 58 3eqtrd 
 |-  ( ( a e. No /\ A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b ) -> ( a +s 0s ) = a )
60 59 ex 
 |-  ( a e. No -> ( A. b e. ( ( _L ` a ) u. ( _R ` a ) ) ( b +s 0s ) = b -> ( a +s 0s ) = a ) )
61 3 6 60 noinds 
 |-  ( A e. No -> ( A +s 0s ) = A )