This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimmptrcl

Description: Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimabs.1 ⊢ φ ∧ k ∈ A → B ∈ V
rlimabs.2 ⊢ φ → k ∈ A ⟼ B ⇝ℝ C
Assertion rlimmptrcl ⊢ φ ∧ k ∈ A → B ∈ ℂ

Proof

Step Hyp Ref Expression
1 rlimabs.1 ⊢ φ ∧ k ∈ A → B ∈ V
2 rlimabs.2 ⊢ φ → k ∈ A ⟼ B ⇝ℝ C
3 rlimf ⊢ k ∈ A ⟼ B ⇝ℝ C → k ∈ A ⟼ B : dom ⁡ k ∈ A ⟼ B ⟶ ℂ
4 2 3 syl ⊢ φ → k ∈ A ⟼ B : dom ⁡ k ∈ A ⟼ B ⟶ ℂ
5 eqid ⊢ k ∈ A ⟼ B = k ∈ A ⟼ B
6 5 1 dmmptd ⊢ φ → dom ⁡ k ∈ A ⟼ B = A
7 6 feq2d ⊢ φ → k ∈ A ⟼ B : dom ⁡ k ∈ A ⟼ B ⟶ ℂ ↔ k ∈ A ⟼ B : A ⟶ ℂ
8 4 7 mpbid ⊢ φ → k ∈ A ⟼ B : A ⟶ ℂ
9 8 fvmptelcdm ⊢ φ ∧ k ∈ A → B ∈ ℂ