| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rnco2 |
|- ran ( [,] o. F ) = ( [,] " ran F ) |
| 2 |
|
ffvelcdm |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( F ` y ) e. ( <_ i^i ( RR X. RR ) ) ) |
| 3 |
2
|
elin2d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( F ` y ) e. ( RR X. RR ) ) |
| 4 |
|
1st2nd2 |
|- ( ( F ` y ) e. ( RR X. RR ) -> ( F ` y ) = <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. ) |
| 5 |
3 4
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( F ` y ) = <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. ) |
| 6 |
5
|
fveq2d |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) = ( [,] ` <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. ) ) |
| 7 |
|
df-ov |
|- ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) = ( [,] ` <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. ) |
| 8 |
6 7
|
eqtr4di |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) = ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) ) |
| 9 |
|
xp1st |
|- ( ( F ` y ) e. ( RR X. RR ) -> ( 1st ` ( F ` y ) ) e. RR ) |
| 10 |
3 9
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( 1st ` ( F ` y ) ) e. RR ) |
| 11 |
|
xp2nd |
|- ( ( F ` y ) e. ( RR X. RR ) -> ( 2nd ` ( F ` y ) ) e. RR ) |
| 12 |
3 11
|
syl |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( 2nd ` ( F ` y ) ) e. RR ) |
| 13 |
|
iccssre |
|- ( ( ( 1st ` ( F ` y ) ) e. RR /\ ( 2nd ` ( F ` y ) ) e. RR ) -> ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) C_ RR ) |
| 14 |
10 12 13
|
syl2anc |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) C_ RR ) |
| 15 |
8 14
|
eqsstrd |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) C_ RR ) |
| 16 |
|
reex |
|- RR e. _V |
| 17 |
16
|
elpw2 |
|- ( ( [,] ` ( F ` y ) ) e. ~P RR <-> ( [,] ` ( F ` y ) ) C_ RR ) |
| 18 |
15 17
|
sylibr |
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) e. ~P RR ) |
| 19 |
18
|
ralrimiva |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> A. y e. NN ( [,] ` ( F ` y ) ) e. ~P RR ) |
| 20 |
|
ffn |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F Fn NN ) |
| 21 |
|
fveq2 |
|- ( x = ( F ` y ) -> ( [,] ` x ) = ( [,] ` ( F ` y ) ) ) |
| 22 |
21
|
eleq1d |
|- ( x = ( F ` y ) -> ( ( [,] ` x ) e. ~P RR <-> ( [,] ` ( F ` y ) ) e. ~P RR ) ) |
| 23 |
22
|
ralrn |
|- ( F Fn NN -> ( A. x e. ran F ( [,] ` x ) e. ~P RR <-> A. y e. NN ( [,] ` ( F ` y ) ) e. ~P RR ) ) |
| 24 |
20 23
|
syl |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( A. x e. ran F ( [,] ` x ) e. ~P RR <-> A. y e. NN ( [,] ` ( F ` y ) ) e. ~P RR ) ) |
| 25 |
19 24
|
mpbird |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> A. x e. ran F ( [,] ` x ) e. ~P RR ) |
| 26 |
|
iccf |
|- [,] : ( RR* X. RR* ) --> ~P RR* |
| 27 |
|
ffun |
|- ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] ) |
| 28 |
26 27
|
ax-mp |
|- Fun [,] |
| 29 |
|
frn |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ ( <_ i^i ( RR X. RR ) ) ) |
| 30 |
|
inss2 |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR ) |
| 31 |
|
rexpssxrxp |
|- ( RR X. RR ) C_ ( RR* X. RR* ) |
| 32 |
30 31
|
sstri |
|- ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) |
| 33 |
26
|
fdmi |
|- dom [,] = ( RR* X. RR* ) |
| 34 |
32 33
|
sseqtrri |
|- ( <_ i^i ( RR X. RR ) ) C_ dom [,] |
| 35 |
29 34
|
sstrdi |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ dom [,] ) |
| 36 |
|
funimass4 |
|- ( ( Fun [,] /\ ran F C_ dom [,] ) -> ( ( [,] " ran F ) C_ ~P RR <-> A. x e. ran F ( [,] ` x ) e. ~P RR ) ) |
| 37 |
28 35 36
|
sylancr |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( [,] " ran F ) C_ ~P RR <-> A. x e. ran F ( [,] ` x ) e. ~P RR ) ) |
| 38 |
25 37
|
mpbird |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( [,] " ran F ) C_ ~P RR ) |
| 39 |
1 38
|
eqsstrid |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ran ( [,] o. F ) C_ ~P RR ) |
| 40 |
|
sspwuni |
|- ( ran ( [,] o. F ) C_ ~P RR <-> U. ran ( [,] o. F ) C_ RR ) |
| 41 |
39 40
|
sylib |
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR ) |