Metamath Proof Explorer

Theorem cncfmpt2f

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

Ref Expression
Hypotheses cncfmpt2f.1 ⊢ J = TopOpen ⁡ ℂ fld
cncfmpt2f.2 ⊢ φ → F ∈ J × t J Cn J
cncfmpt2f.3 ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
cncfmpt2f.4 ⊢ φ → x ∈ X ⟼ B : X ⟶cn ℂ
Assertion cncfmpt2f ⊢ φ → x ∈ X ⟼ A F B : X ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 cncfmpt2f.1 ⊢ J = TopOpen ⁡ ℂ fld
2 cncfmpt2f.2 ⊢ φ → F ∈ J × t J Cn J
3 cncfmpt2f.3 ⊢ φ → x ∈ X ⟼ A : X ⟶cn ℂ
4 cncfmpt2f.4 ⊢ φ → x ∈ X ⟼ B : X ⟶cn ℂ
5 1 cnfldtopon ⊢ J ∈ TopOn ⁡ ℂ
6 cncfrss ⊢ x ∈ X ⟼ A : X ⟶cn ℂ → X ⊆ ℂ
7 3 6 syl ⊢ φ → X ⊆ ℂ
8 resttopon ⊢ J ∈ TopOn ⁡ ℂ ∧ X ⊆ ℂ → J ↾ 𝑡 X ∈ TopOn ⁡ X
9 5 7 8 sylancr ⊢ φ → J ↾ 𝑡 X ∈ TopOn ⁡ X
10 ssid ⊢ ℂ ⊆ ℂ
11 eqid ⊢ J ↾ 𝑡 X = J ↾ 𝑡 X
12 5 toponrestid ⊢ J = J ↾ 𝑡 ℂ
13 1 11 12 cncfcn ⊢ X ⊆ ℂ ∧ ℂ ⊆ ℂ → X ⟶cn ℂ = J ↾ 𝑡 X Cn J
14 7 10 13 sylancl ⊢ φ → X ⟶cn ℂ = J ↾ 𝑡 X Cn J
15 3 14 eleqtrd ⊢ φ → x ∈ X ⟼ A ∈ J ↾ 𝑡 X Cn J
16 4 14 eleqtrd ⊢ φ → x ∈ X ⟼ B ∈ J ↾ 𝑡 X Cn J
17 9 15 16 2 cnmpt12f ⊢ φ → x ∈ X ⟼ A F B ∈ J ↾ 𝑡 X Cn J
18 17 14 eleqtrrd ⊢ φ → x ∈ X ⟼ A F B : X ⟶cn ℂ