This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimcn1b

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 10-May-2016)

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

Proof

Step Hyp Ref Expression
1 rlimcn1b.1 
 |-  ( ( ph /\ k e. A ) -> B e. X )
2 rlimcn1b.2 
 |-  ( ph -> C e. X )
3 rlimcn1b.3 
 |-  ( ph -> ( k e. A |-> B ) ~~>r C )
4 rlimcn1b.4 
 |-  ( ph -> F : X --> CC )
5 rlimcn1b.5 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. X ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` C ) ) ) < x ) )
6 4 1 cofmpt 
 |-  ( ph -> ( F o. ( k e. A |-> B ) ) = ( k e. A |-> ( F ` B ) ) )
7 1 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> X )
8 7 2 3 4 5 rlimcn1 
 |-  ( ph -> ( F o. ( k e. A |-> B ) ) ~~>r ( F ` C ) )
9 6 8 eqbrtrrd 
 |-  ( ph -> ( k e. A |-> ( F ` B ) ) ~~>r ( F ` C ) )