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