Metamath Proof Explorer

Theorem climcncf

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses climcncf.1 
|- Z = ( ZZ>= ` M )
climcncf.2 
|- ( ph -> M e. ZZ )
climcncf.4 
|- ( ph -> F e. ( A -cn-> B ) )
climcncf.5 
|- ( ph -> G : Z --> A )
climcncf.6 
|- ( ph -> G ~~> D )
climcncf.7 
|- ( ph -> D e. A )
Assertion climcncf 
|- ( ph -> ( F o. G ) ~~> ( F ` D ) )

Proof

Step Hyp Ref Expression
1 climcncf.1 
 |-  Z = ( ZZ>= ` M )
2 climcncf.2 
 |-  ( ph -> M e. ZZ )
3 climcncf.4 
 |-  ( ph -> F e. ( A -cn-> B ) )
4 climcncf.5 
 |-  ( ph -> G : Z --> A )
5 climcncf.6 
 |-  ( ph -> G ~~> D )
6 climcncf.7 
 |-  ( ph -> D e. A )
7 cncff 
 |-  ( F e. ( A -cn-> B ) -> F : A --> B )
8 3 7 syl 
 |-  ( ph -> F : A --> B )
9 8 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. B )
10 cncfrss2 
 |-  ( F e. ( A -cn-> B ) -> B C_ CC )
11 3 10 syl 
 |-  ( ph -> B C_ CC )
12 11 sselda 
 |-  ( ( ph /\ ( F ` z ) e. B ) -> ( F ` z ) e. CC )
13 9 12 syldan 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. CC )
14 1 fvexi 
 |-  Z e. _V
15 fex 
 |-  ( ( G : Z --> A /\ Z e. _V ) -> G e. _V )
16 4 14 15 sylancl 
 |-  ( ph -> G e. _V )
17 coexg 
 |-  ( ( F e. ( A -cn-> B ) /\ G e. _V ) -> ( F o. G ) e. _V )
18 3 16 17 syl2anc 
 |-  ( ph -> ( F o. G ) e. _V )
19 cncfi 
 |-  ( ( F e. ( A -cn-> B ) /\ D e. A /\ x e. RR+ ) -> E. y e. RR+ A. z e. A ( ( abs ` ( z - D ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` D ) ) ) < x ) )
20 19 3expia 
 |-  ( ( F e. ( A -cn-> B ) /\ D e. A ) -> ( x e. RR+ -> E. y e. RR+ A. z e. A ( ( abs ` ( z - D ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` D ) ) ) < x ) ) )
21 3 6 20 syl2anc 
 |-  ( ph -> ( x e. RR+ -> E. y e. RR+ A. z e. A ( ( abs ` ( z - D ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` D ) ) ) < x ) ) )
22 21 imp 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. A ( ( abs ` ( z - D ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` D ) ) ) < x ) )
23 4 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. A )
24 fvco3 
 |-  ( ( G : Z --> A /\ k e. Z ) -> ( ( F o. G ) ` k ) = ( F ` ( G ` k ) ) )
25 4 24 sylan 
 |-  ( ( ph /\ k e. Z ) -> ( ( F o. G ) ` k ) = ( F ` ( G ` k ) ) )
26 1 2 6 13 5 18 22 23 25 climcn1 
 |-  ( ph -> ( F o. G ) ~~> ( F ` D ) )