Step |
Hyp |
Ref |
Expression |
1 |
|
negf1o.1 |
|- F = ( x e. A |-> -u x ) |
2 |
|
negeq |
|- ( n = -u x -> -u n = -u -u x ) |
3 |
2
|
eleq1d |
|- ( n = -u x -> ( -u n e. A <-> -u -u x e. A ) ) |
4 |
|
ssel |
|- ( A C_ RR -> ( x e. A -> x e. RR ) ) |
5 |
|
renegcl |
|- ( x e. RR -> -u x e. RR ) |
6 |
4 5
|
syl6 |
|- ( A C_ RR -> ( x e. A -> -u x e. RR ) ) |
7 |
6
|
imp |
|- ( ( A C_ RR /\ x e. A ) -> -u x e. RR ) |
8 |
4
|
imp |
|- ( ( A C_ RR /\ x e. A ) -> x e. RR ) |
9 |
|
recn |
|- ( x e. RR -> x e. CC ) |
10 |
|
negneg |
|- ( x e. CC -> -u -u x = x ) |
11 |
10
|
eqcomd |
|- ( x e. CC -> x = -u -u x ) |
12 |
9 11
|
syl |
|- ( x e. RR -> x = -u -u x ) |
13 |
12
|
eleq1d |
|- ( x e. RR -> ( x e. A <-> -u -u x e. A ) ) |
14 |
13
|
biimpcd |
|- ( x e. A -> ( x e. RR -> -u -u x e. A ) ) |
15 |
14
|
adantl |
|- ( ( A C_ RR /\ x e. A ) -> ( x e. RR -> -u -u x e. A ) ) |
16 |
8 15
|
mpd |
|- ( ( A C_ RR /\ x e. A ) -> -u -u x e. A ) |
17 |
3 7 16
|
elrabd |
|- ( ( A C_ RR /\ x e. A ) -> -u x e. { n e. RR | -u n e. A } ) |
18 |
|
negeq |
|- ( n = y -> -u n = -u y ) |
19 |
18
|
eleq1d |
|- ( n = y -> ( -u n e. A <-> -u y e. A ) ) |
20 |
19
|
elrab |
|- ( y e. { n e. RR | -u n e. A } <-> ( y e. RR /\ -u y e. A ) ) |
21 |
|
simpr |
|- ( ( y e. RR /\ -u y e. A ) -> -u y e. A ) |
22 |
21
|
a1i |
|- ( A C_ RR -> ( ( y e. RR /\ -u y e. A ) -> -u y e. A ) ) |
23 |
20 22
|
syl5bi |
|- ( A C_ RR -> ( y e. { n e. RR | -u n e. A } -> -u y e. A ) ) |
24 |
23
|
imp |
|- ( ( A C_ RR /\ y e. { n e. RR | -u n e. A } ) -> -u y e. A ) |
25 |
4 9
|
syl6com |
|- ( x e. A -> ( A C_ RR -> x e. CC ) ) |
26 |
25
|
adantl |
|- ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) -> ( A C_ RR -> x e. CC ) ) |
27 |
26
|
imp |
|- ( ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) /\ A C_ RR ) -> x e. CC ) |
28 |
|
recn |
|- ( y e. RR -> y e. CC ) |
29 |
28
|
ad3antrrr |
|- ( ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) /\ A C_ RR ) -> y e. CC ) |
30 |
|
negcon2 |
|- ( ( x e. CC /\ y e. CC ) -> ( x = -u y <-> y = -u x ) ) |
31 |
27 29 30
|
syl2anc |
|- ( ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) /\ A C_ RR ) -> ( x = -u y <-> y = -u x ) ) |
32 |
31
|
exp31 |
|- ( ( y e. RR /\ -u y e. A ) -> ( x e. A -> ( A C_ RR -> ( x = -u y <-> y = -u x ) ) ) ) |
33 |
20 32
|
sylbi |
|- ( y e. { n e. RR | -u n e. A } -> ( x e. A -> ( A C_ RR -> ( x = -u y <-> y = -u x ) ) ) ) |
34 |
33
|
impcom |
|- ( ( x e. A /\ y e. { n e. RR | -u n e. A } ) -> ( A C_ RR -> ( x = -u y <-> y = -u x ) ) ) |
35 |
34
|
impcom |
|- ( ( A C_ RR /\ ( x e. A /\ y e. { n e. RR | -u n e. A } ) ) -> ( x = -u y <-> y = -u x ) ) |
36 |
1 17 24 35
|
f1o2d |
|- ( A C_ RR -> F : A -1-1-onto-> { n e. RR | -u n e. A } ) |