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 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
rlimcn1b.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
rlimcn1b.3 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
rlimcn1b.4 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
rlimcn1b.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
Assertion rlimcn1b ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rlimcn1b.1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
2 rlimcn1b.2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
3 rlimcn1b.3 ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
4 rlimcn1b.4 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
5 rlimcn1b.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ( ( abs ‘ ( 𝑧 − 𝐶 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝑥 ) )
6 4 1 cofmpt ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) )
7 1 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑋 )
8 7 2 3 4 5 rlimcn1 ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )
9 6 8 eqbrtrrd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ⇝𝑟 ( 𝐹 ‘ 𝐶 ) )