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

Metamath Proof Explorer

Theorem cncfmpt1f

Description: Composition of continuous functions. -cn-> analogue of cnmpt11f . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses cncfmpt1f.1 ⊢ φ → F : ℂ ⟶cn ℂ
cncfmpt1f.2 ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
Assertion cncfmpt1f ⊢ φ → x ∈ X ⟼ F ⁡ A : X ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 cncfmpt1f.1 ⊢ φ → F : ℂ ⟶cn ℂ
2 cncfmpt1f.2 ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
3 cncff ⊢ x ∈ X ⟼ A : X ⟶cn ℂ → x ∈ X ⟼ A : X ⟶ ℂ
4 2 3 syl ⊢ φ → x ∈ X ⟼ A : X ⟶ ℂ
5 eqid ⊢ x ∈ X ⟼ A = x ∈ X ⟼ A
6 5 fmpt ⊢ ∀ x ∈ X A ∈ ℂ ↔ x ∈ X ⟼ A : X ⟶ ℂ
7 4 6 sylibr ⊢ φ → ∀ x ∈ X A ∈ ℂ
8 eqidd ⊢ φ → x ∈ X ⟼ A = x ∈ X ⟼ A
9 cncff ⊢ F : ℂ ⟶cn ℂ → F : ℂ ⟶ ℂ
10 1 9 syl ⊢ φ → F : ℂ ⟶ ℂ
11 10 feqmptd ⊢ φ → F = y ∈ ℂ ⟼ F ⁡ y
12 fveq2 ⊢ y = A → F ⁡ y = F ⁡ A
13 7 8 11 12 fmptcof ⊢ φ → F ∘ x ∈ X ⟼ A = x ∈ X ⟼ F ⁡ A
14 2 1 cncfco ⊢ φ → F ∘ x ∈ X ⟼ A : X ⟶cn ℂ
15 13 14 eqeltrrd ⊢ φ → x ∈ X ⟼ F ⁡ A : X ⟶cn ℂ