Metamath Proof Explorer

Theorem rlimcn1

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 17-Sep-2014)

Ref Expression
Hypotheses rlimcn1.1 
|- ( ph -> G : A --> X )
rlimcn1.2 
|- ( ph -> C e. X )
rlimcn1.3 
|- ( ph -> G ~~>r C )
rlimcn1.4 
|- ( ph -> F : X --> CC )
rlimcn1.5 
|- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )
Assertion rlimcn1 
|- ( ph -> ( F o. G ) ~~>r ( F ` C ) )

Proof

Step Hyp Ref Expression
1 rlimcn1.1 
 |-  ( ph -> G : A --> X )
2 rlimcn1.2 
 |-  ( ph -> C e. X )
3 rlimcn1.3 
 |-  ( ph -> G ~~>r C )
4 rlimcn1.4 
 |-  ( ph -> F : X --> CC )
5 rlimcn1.5 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )
6 1 ffvelrnda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. X )
7 1 feqmptd 
 |-  ( ph -> G = ( w e. A |-> ( G ` w ) ) )
8 4 feqmptd 
 |-  ( ph -> F = ( v e. X |-> ( F ` v ) ) )
9 fveq2 
 |-  ( v = ( G ` w ) -> ( F ` v ) = ( F ` ( G ` w ) ) )
10 6 7 8 9 fmptco 
 |-  ( ph -> ( F o. G ) = ( w e. A |-> ( F ` ( G ` w ) ) ) )
11 fvexd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) /\ w e. A ) -> ( G ` w ) e. _V )
12 11 ralrimiva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) -> A. w e. A ( G ` w ) e. _V )
13 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) -> y e. RR+ )
14 7 3 eqbrtrrd 
 |-  ( ph -> ( w e. A |-> ( G ` w ) ) ~~>r C )
15 14 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) -> ( w e. A |-> ( G ` w ) ) ~~>r C )
16 12 13 15 rlimi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) -> E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( G ` w ) - C ) ) < y ) )
17 fvoveq1 
 |-  ( z = ( G ` w ) -> ( abs ` ( z - C ) ) = ( abs ` ( ( G ` w ) - C ) ) )
18 17 breq1d 
 |-  ( z = ( G ` w ) -> ( ( abs ` ( z - C ) ) < y <-> ( abs ` ( ( G ` w ) - C ) ) < y ) )
19 18 imbrov2fvoveq 
 |-  ( z = ( G ` w ) -> ( ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) <-> ( ( abs ` ( ( G ` w ) - C ) ) < y -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
20 simplrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( y e. RR+ /\ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) ) ) /\ w e. A ) -> A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )
21 6 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( y e. RR+ /\ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) ) ) /\ w e. A ) -> ( G ` w ) e. X )
22 19 20 21 rspcdva 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( y e. RR+ /\ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) ) ) /\ w e. A ) -> ( ( abs ` ( ( G ` w ) - C ) ) < y -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) )
23 22 imim2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ ( y e. RR+ /\ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) ) ) /\ w e. A ) -> ( ( c <_ w -> ( abs ` ( ( G ` w ) - C ) ) < y ) -> ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
24 23 ralimdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( y e. RR+ /\ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) ) ) -> ( A. w e. A ( c <_ w -> ( abs ` ( ( G ` w ) - C ) ) < y ) -> A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
25 24 reximdv 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( y e. RR+ /\ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) ) ) -> ( E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( G ` w ) - C ) ) < y ) -> E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
26 25 expr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) -> ( A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) -> ( E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( G ` w ) - C ) ) < y ) -> E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) ) )
27 16 26 mpid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ y e. RR+ ) -> ( A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) -> E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
28 27 rexlimdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) -> E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
29 5 28 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) )
30 29 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) )
31 4 ffvelrnda 
 |-  ( ( ph /\ ( G ` w ) e. X ) -> ( F ` ( G ` w ) ) e. CC )
32 6 31 syldan 
 |-  ( ( ph /\ w e. A ) -> ( F ` ( G ` w ) ) e. CC )
33 32 ralrimiva 
 |-  ( ph -> A. w e. A ( F ` ( G ` w ) ) e. CC )
34 1 fdmd 
 |-  ( ph -> dom G = A )
35 rlimss 
 |-  ( G ~~>r C -> dom G C_ RR )
36 3 35 syl 
 |-  ( ph -> dom G C_ RR )
37 34 36 eqsstrrd 
 |-  ( ph -> A C_ RR )
38 4 2 ffvelrnd 
 |-  ( ph -> ( F ` C ) e. CC )
39 33 37 38 rlim2 
 |-  ( ph -> ( ( w e. A |-> ( F ` ( G ` w ) ) ) ~~>r ( F ` C ) <-> A. x e. RR+ E. c e. RR A. w e. A ( c <_ w -> ( abs ` ( ( F ` ( G ` w ) ) - ( F ` C ) ) ) < x ) ) )
40 30 39 mpbird 
 |-  ( ph -> ( w e. A |-> ( F ` ( G ` w ) ) ) ~~>r ( F ` C ) )
41 10 40 eqbrtrd 
 |-  ( ph -> ( F o. G ) ~~>r ( F ` C ) )