Theorem rlimcn2

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

	Ref	Expression
Hypotheses	rlimcn2.1a	|- ( ( ph /\ z e. A ) -> B e. X )
	rlimcn2.1b	|- ( ( ph /\ z e. A ) -> C e. Y )
	rlimcn2.2a	|- ( ph -> R e. X )
	rlimcn2.2b	|- ( ph -> S e. Y )
	rlimcn2.3a	|- ( ph -> ( z e. A |-> B ) ~~>r R )
	rlimcn2.3b	|- ( ph -> ( z e. A |-> C ) ~~>r S )
	rlimcn2.4	|- ( ph -> F : ( X X. Y ) --> CC )
	rlimcn2.5	|- ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )
Assertion	rlimcn2	|- ( ph -> ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) )

Proof

Step	Hyp	Ref	Expression
1		rlimcn2.1a	|- ( ( ph /\ z e. A ) -> B e. X )
2		rlimcn2.1b	|- ( ( ph /\ z e. A ) -> C e. Y )
3		rlimcn2.2a	|- ( ph -> R e. X )
4		rlimcn2.2b	|- ( ph -> S e. Y )
5		rlimcn2.3a	|- ( ph -> ( z e. A |-> B ) ~~>r R )
6		rlimcn2.3b	|- ( ph -> ( z e. A |-> C ) ~~>r S )
7		rlimcn2.4	|- ( ph -> F : ( X X. Y ) --> CC )
8		rlimcn2.5	|- ( ( ph /\ x e. RR+ ) -> E. r e. RR+ E. s e. RR+ A. u e. X A. v e. Y ( ( ( abs ` ( u - R ) ) < r /\ ( abs ` ( v - S ) ) < s ) -> ( abs ` ( ( u F v ) - ( R F S ) ) ) < x ) )
9	7	adantr	|- ( ( ph /\ z e. A ) -> F : ( X X. Y ) --> CC )
10	9 1 2	fovrnd	|- ( ( ph /\ z e. A ) -> ( B F C ) e. CC )
11	7 3 4	fovrnd	|- ( ph -> ( R F S ) e. CC )
12	1 2 10 11 5 6 8	rlimcn3	|- ( ph -> ( z e. A |-> ( B F C ) ) ~~>r ( R F S ) )