Metamath Proof Explorer

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 ⊢ φ ∧ z ∈ A → B ∈ X
rlimcn2.1b ⊢ φ ∧ z ∈ A → C ∈ Y
rlimcn2.2a ⊢ φ → R ∈ X
rlimcn2.2b ⊢ φ → S ∈ Y
rlimcn2.3a ⊢ φ → z ∈ A ⟼ B ⇝ℝ R
rlimcn2.3b ⊢ φ → z ∈ A ⟼ C ⇝ℝ S
rlimcn2.4 ⊢ φ → F : X × Y ⟶ ℂ
rlimcn2.5 ⊢ φ ∧ x ∈ ℝ + → ∃ r ∈ ℝ + ∃ s ∈ ℝ + ∀ u ∈ X ∀ v ∈ Y u − R < r ∧ v − S < s → u F v − R F S < x
Assertion rlimcn2 ⊢ φ → z ∈ A ⟼ B F C ⇝ℝ R F S

Proof

Step Hyp Ref Expression
1 rlimcn2.1a ⊢ φ ∧ z ∈ A → B ∈ X
2 rlimcn2.1b ⊢ φ ∧ z ∈ A → C ∈ Y
3 rlimcn2.2a ⊢ φ → R ∈ X
4 rlimcn2.2b ⊢ φ → S ∈ Y
5 rlimcn2.3a ⊢ φ → z ∈ A ⟼ B ⇝ℝ R
6 rlimcn2.3b ⊢ φ → z ∈ A ⟼ C ⇝ℝ S
7 rlimcn2.4 ⊢ φ → F : X × Y ⟶ ℂ
8 rlimcn2.5 ⊢ φ ∧ x ∈ ℝ + → ∃ r ∈ ℝ + ∃ s ∈ ℝ + ∀ u ∈ X ∀ v ∈ Y u − R < r ∧ v − S < s → u F v − R F S < x
9 7 adantr ⊢ φ ∧ z ∈ A → F : X × Y ⟶ ℂ
10 9 1 2 fovrnd ⊢ φ ∧ z ∈ A → B F C ∈ ℂ
11 7 3 4 fovrnd ⊢ φ → R F S ∈ ℂ
12 1 2 10 11 5 6 8 rlimcn3 ⊢ φ → z ∈ A ⟼ B F C ⇝ℝ R F S