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	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
	rlimcn2.1b	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝑌 )
	rlimcn2.2a	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
	rlimcn2.2b	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
	rlimcn2.3a	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝑅 )
	rlimcn2.3b	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝑆 )
	rlimcn2.4	⊢ ( 𝜑 → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
	rlimcn2.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
Assertion	rlimcn2	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ ( 𝐵 𝐹 𝐶 ) ) ⇝𝑟 ( 𝑅 𝐹 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		rlimcn2.1a	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
2		rlimcn2.1b	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐶 ∈ 𝑌 )
3		rlimcn2.2a	⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
4		rlimcn2.2b	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
5		rlimcn2.3a	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝑅 )
6		rlimcn2.3b	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝑆 )
7		rlimcn2.4	⊢ ( 𝜑 → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
8		rlimcn2.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( abs ‘ ( 𝑢 − 𝑅 ) ) < 𝑟 ∧ ( abs ‘ ( 𝑣 − 𝑆 ) ) < 𝑠 ) → ( abs ‘ ( ( 𝑢 𝐹 𝑣 ) − ( 𝑅 𝐹 𝑆 ) ) ) < 𝑥 ) )
9	7	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ ℂ )
10	9 1 2	fovrnd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐵 𝐹 𝐶 ) ∈ ℂ )
11	7 3 4	fovrnd	⊢ ( 𝜑 → ( 𝑅 𝐹 𝑆 ) ∈ ℂ )
12	1 2 10 11 5 6 8	rlimcn3	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 ↦ ( 𝐵 𝐹 𝐶 ) ) ⇝𝑟 ( 𝑅 𝐹 𝑆 ) )