Step |
Hyp |
Ref |
Expression |
1 |
|
riotaneg.1 |
|- ( x = -u y -> ( ph <-> ps ) ) |
2 |
|
tru |
|- T. |
3 |
|
nfriota1 |
|- F/_ y ( iota_ y e. RR ps ) |
4 |
3
|
nfneg |
|- F/_ y -u ( iota_ y e. RR ps ) |
5 |
|
renegcl |
|- ( y e. RR -> -u y e. RR ) |
6 |
5
|
adantl |
|- ( ( T. /\ y e. RR ) -> -u y e. RR ) |
7 |
|
simpr |
|- ( ( T. /\ ( iota_ y e. RR ps ) e. RR ) -> ( iota_ y e. RR ps ) e. RR ) |
8 |
7
|
renegcld |
|- ( ( T. /\ ( iota_ y e. RR ps ) e. RR ) -> -u ( iota_ y e. RR ps ) e. RR ) |
9 |
|
negeq |
|- ( y = ( iota_ y e. RR ps ) -> -u y = -u ( iota_ y e. RR ps ) ) |
10 |
|
renegcl |
|- ( x e. RR -> -u x e. RR ) |
11 |
|
recn |
|- ( x e. RR -> x e. CC ) |
12 |
|
recn |
|- ( y e. RR -> y e. CC ) |
13 |
|
negcon2 |
|- ( ( x e. CC /\ y e. CC ) -> ( x = -u y <-> y = -u x ) ) |
14 |
11 12 13
|
syl2an |
|- ( ( x e. RR /\ y e. RR ) -> ( x = -u y <-> y = -u x ) ) |
15 |
10 14
|
reuhyp |
|- ( x e. RR -> E! y e. RR x = -u y ) |
16 |
15
|
adantl |
|- ( ( T. /\ x e. RR ) -> E! y e. RR x = -u y ) |
17 |
4 6 8 1 9 16
|
riotaxfrd |
|- ( ( T. /\ E! x e. RR ph ) -> ( iota_ x e. RR ph ) = -u ( iota_ y e. RR ps ) ) |
18 |
2 17
|
mpan |
|- ( E! x e. RR ph -> ( iota_ x e. RR ph ) = -u ( iota_ y e. RR ps ) ) |