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

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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cncfmpt2f.2 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
cncfmpt2f.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
cncfmpt2f.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion cncfmpt2f ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 cncfmpt2f.1 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 cncfmpt2f.2 ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
3 cncfmpt2f.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
4 cncfmpt2f.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
5 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
6 cncfrss ⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) → 𝑋 ⊆ ℂ )
7 3 6 syl ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
8 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑋 ⊆ ℂ ) → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
9 5 7 8 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑋 ) ∈ ( TopOn ‘ 𝑋 ) )
10 ssid ⊢ ℂ ⊆ ℂ
11 eqid ⊢ ( 𝐽 ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 )
12 5 toponrestid ⊢ 𝐽 = ( 𝐽 ↾t ℂ )
13 1 11 12 cncfcn ⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋 –cn→ ℂ ) = ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
14 7 10 13 sylancl ⊢ ( 𝜑 → ( 𝑋 –cn→ ℂ ) = ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
15 3 14 eleqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
16 4 14 eleqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
17 9 15 16 2 cnmpt12f ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( ( 𝐽 ↾t 𝑋 ) Cn 𝐽 ) )
18 17 14 eleqtrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )