Step |
Hyp |
Ref |
Expression |
1 |
|
sinf |
|- sin : CC --> CC |
2 |
|
ffn |
|- ( sin : CC --> CC -> sin Fn CC ) |
3 |
1 2
|
ax-mp |
|- sin Fn CC |
4 |
|
ax-resscn |
|- RR C_ CC |
5 |
|
fnssres |
|- ( ( sin Fn CC /\ RR C_ CC ) -> ( sin |` RR ) Fn RR ) |
6 |
3 4 5
|
mp2an |
|- ( sin |` RR ) Fn RR |
7 |
|
fvres |
|- ( x e. RR -> ( ( sin |` RR ) ` x ) = ( sin ` x ) ) |
8 |
|
resincl |
|- ( x e. RR -> ( sin ` x ) e. RR ) |
9 |
7 8
|
eqeltrd |
|- ( x e. RR -> ( ( sin |` RR ) ` x ) e. RR ) |
10 |
9
|
rgen |
|- A. x e. RR ( ( sin |` RR ) ` x ) e. RR |
11 |
|
ffnfv |
|- ( ( sin |` RR ) : RR --> RR <-> ( ( sin |` RR ) Fn RR /\ A. x e. RR ( ( sin |` RR ) ` x ) e. RR ) ) |
12 |
6 10 11
|
mpbir2an |
|- ( sin |` RR ) : RR --> RR |
13 |
|
sincn |
|- sin e. ( CC -cn-> CC ) |
14 |
|
rescncf |
|- ( RR C_ CC -> ( sin e. ( CC -cn-> CC ) -> ( sin |` RR ) e. ( RR -cn-> CC ) ) ) |
15 |
4 13 14
|
mp2 |
|- ( sin |` RR ) e. ( RR -cn-> CC ) |
16 |
|
cncffvrn |
|- ( ( RR C_ CC /\ ( sin |` RR ) e. ( RR -cn-> CC ) ) -> ( ( sin |` RR ) e. ( RR -cn-> RR ) <-> ( sin |` RR ) : RR --> RR ) ) |
17 |
4 15 16
|
mp2an |
|- ( ( sin |` RR ) e. ( RR -cn-> RR ) <-> ( sin |` RR ) : RR --> RR ) |
18 |
12 17
|
mpbir |
|- ( sin |` RR ) e. ( RR -cn-> RR ) |