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 ) )