Step |
Hyp |
Ref |
Expression |
1 |
|
ssel |
|- ( A C_ RR -> ( a e. A -> a e. RR ) ) |
2 |
|
renegcl |
|- ( a e. RR -> -u a e. RR ) |
3 |
1 2
|
syl6 |
|- ( A C_ RR -> ( a e. A -> -u a e. RR ) ) |
4 |
3
|
ralrimiv |
|- ( A C_ RR -> A. a e. A -u a e. RR ) |
5 |
|
dmmptg |
|- ( A. a e. A -u a e. RR -> dom ( a e. A |-> -u a ) = A ) |
6 |
4 5
|
syl |
|- ( A C_ RR -> dom ( a e. A |-> -u a ) = A ) |
7 |
6
|
eqcomd |
|- ( A C_ RR -> A = dom ( a e. A |-> -u a ) ) |
8 |
7
|
eleq1d |
|- ( A C_ RR -> ( A e. Fin <-> dom ( a e. A |-> -u a ) e. Fin ) ) |
9 |
|
funmpt |
|- Fun ( a e. A |-> -u a ) |
10 |
|
fundmfibi |
|- ( Fun ( a e. A |-> -u a ) -> ( ( a e. A |-> -u a ) e. Fin <-> dom ( a e. A |-> -u a ) e. Fin ) ) |
11 |
9 10
|
mp1i |
|- ( A C_ RR -> ( ( a e. A |-> -u a ) e. Fin <-> dom ( a e. A |-> -u a ) e. Fin ) ) |
12 |
8 11
|
bitr4d |
|- ( A C_ RR -> ( A e. Fin <-> ( a e. A |-> -u a ) e. Fin ) ) |
13 |
|
reex |
|- RR e. _V |
14 |
13
|
ssex |
|- ( A C_ RR -> A e. _V ) |
15 |
14
|
mptexd |
|- ( A C_ RR -> ( a e. A |-> -u a ) e. _V ) |
16 |
|
eqid |
|- ( a e. A |-> -u a ) = ( a e. A |-> -u a ) |
17 |
16
|
negf1o |
|- ( A C_ RR -> ( a e. A |-> -u a ) : A -1-1-onto-> { x e. RR | -u x e. A } ) |
18 |
|
f1of1 |
|- ( ( a e. A |-> -u a ) : A -1-1-onto-> { x e. RR | -u x e. A } -> ( a e. A |-> -u a ) : A -1-1-> { x e. RR | -u x e. A } ) |
19 |
17 18
|
syl |
|- ( A C_ RR -> ( a e. A |-> -u a ) : A -1-1-> { x e. RR | -u x e. A } ) |
20 |
|
f1vrnfibi |
|- ( ( ( a e. A |-> -u a ) e. _V /\ ( a e. A |-> -u a ) : A -1-1-> { x e. RR | -u x e. A } ) -> ( ( a e. A |-> -u a ) e. Fin <-> ran ( a e. A |-> -u a ) e. Fin ) ) |
21 |
15 19 20
|
syl2anc |
|- ( A C_ RR -> ( ( a e. A |-> -u a ) e. Fin <-> ran ( a e. A |-> -u a ) e. Fin ) ) |
22 |
1
|
imp |
|- ( ( A C_ RR /\ a e. A ) -> a e. RR ) |
23 |
2
|
adantl |
|- ( ( ( A C_ RR /\ a e. A ) /\ a e. RR ) -> -u a e. RR ) |
24 |
|
recn |
|- ( a e. RR -> a e. CC ) |
25 |
24
|
negnegd |
|- ( a e. RR -> -u -u a = a ) |
26 |
25
|
eqcomd |
|- ( a e. RR -> a = -u -u a ) |
27 |
26
|
eleq1d |
|- ( a e. RR -> ( a e. A <-> -u -u a e. A ) ) |
28 |
27
|
biimpcd |
|- ( a e. A -> ( a e. RR -> -u -u a e. A ) ) |
29 |
28
|
adantl |
|- ( ( A C_ RR /\ a e. A ) -> ( a e. RR -> -u -u a e. A ) ) |
30 |
29
|
imp |
|- ( ( ( A C_ RR /\ a e. A ) /\ a e. RR ) -> -u -u a e. A ) |
31 |
23 30
|
jca |
|- ( ( ( A C_ RR /\ a e. A ) /\ a e. RR ) -> ( -u a e. RR /\ -u -u a e. A ) ) |
32 |
22 31
|
mpdan |
|- ( ( A C_ RR /\ a e. A ) -> ( -u a e. RR /\ -u -u a e. A ) ) |
33 |
|
eleq1 |
|- ( n = -u a -> ( n e. RR <-> -u a e. RR ) ) |
34 |
|
negeq |
|- ( n = -u a -> -u n = -u -u a ) |
35 |
34
|
eleq1d |
|- ( n = -u a -> ( -u n e. A <-> -u -u a e. A ) ) |
36 |
33 35
|
anbi12d |
|- ( n = -u a -> ( ( n e. RR /\ -u n e. A ) <-> ( -u a e. RR /\ -u -u a e. A ) ) ) |
37 |
32 36
|
syl5ibrcom |
|- ( ( A C_ RR /\ a e. A ) -> ( n = -u a -> ( n e. RR /\ -u n e. A ) ) ) |
38 |
37
|
rexlimdva |
|- ( A C_ RR -> ( E. a e. A n = -u a -> ( n e. RR /\ -u n e. A ) ) ) |
39 |
|
simprr |
|- ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> -u n e. A ) |
40 |
|
negeq |
|- ( a = -u n -> -u a = -u -u n ) |
41 |
40
|
eqeq2d |
|- ( a = -u n -> ( n = -u a <-> n = -u -u n ) ) |
42 |
41
|
adantl |
|- ( ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) /\ a = -u n ) -> ( n = -u a <-> n = -u -u n ) ) |
43 |
|
recn |
|- ( n e. RR -> n e. CC ) |
44 |
|
negneg |
|- ( n e. CC -> -u -u n = n ) |
45 |
44
|
eqcomd |
|- ( n e. CC -> n = -u -u n ) |
46 |
43 45
|
syl |
|- ( n e. RR -> n = -u -u n ) |
47 |
46
|
ad2antrl |
|- ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> n = -u -u n ) |
48 |
39 42 47
|
rspcedvd |
|- ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> E. a e. A n = -u a ) |
49 |
48
|
ex |
|- ( A C_ RR -> ( ( n e. RR /\ -u n e. A ) -> E. a e. A n = -u a ) ) |
50 |
38 49
|
impbid |
|- ( A C_ RR -> ( E. a e. A n = -u a <-> ( n e. RR /\ -u n e. A ) ) ) |
51 |
50
|
abbidv |
|- ( A C_ RR -> { n | E. a e. A n = -u a } = { n | ( n e. RR /\ -u n e. A ) } ) |
52 |
16
|
rnmpt |
|- ran ( a e. A |-> -u a ) = { n | E. a e. A n = -u a } |
53 |
|
df-rab |
|- { n e. RR | -u n e. A } = { n | ( n e. RR /\ -u n e. A ) } |
54 |
51 52 53
|
3eqtr4g |
|- ( A C_ RR -> ran ( a e. A |-> -u a ) = { n e. RR | -u n e. A } ) |
55 |
54
|
eleq1d |
|- ( A C_ RR -> ( ran ( a e. A |-> -u a ) e. Fin <-> { n e. RR | -u n e. A } e. Fin ) ) |
56 |
12 21 55
|
3bitrd |
|- ( A C_ RR -> ( A e. Fin <-> { n e. RR | -u n e. A } e. Fin ) ) |
57 |
56
|
biimpa |
|- ( ( A C_ RR /\ A e. Fin ) -> { n e. RR | -u n e. A } e. Fin ) |