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

Metamath Proof Explorer

Theorem cncfcompt

Description: Composition of continuous functions. A generalization of cncfmpt1f to arbitrary domains. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfcompt.bcn ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
cncfcompt.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) )
Assertion cncfcompt ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 cncfcompt.bcn ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
2 cncfcompt.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) )
3 cncff ⊢ ( 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) → 𝐹 : 𝐶 ⟶ 𝐷 )
4 2 3 syl ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐷 )
5 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐶 ⟶ 𝐷 )
6 cncff ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ 𝐶 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
7 1 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
8 7 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
9 5 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ 𝐷 )
10 9 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ 𝐷 )
11 cncfrss2 ⊢ ( 𝐹 ∈ ( 𝐶 –cn→ 𝐷 ) → 𝐷 ⊆ ℂ )
12 2 11 syl ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
13 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
14 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
15 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
16 8 13 14 15 fmptco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) )
17 ssid ⊢ ℂ ⊆ ℂ
18 cncfss ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐶 –cn→ 𝐷 ) ⊆ ( 𝐶 –cn→ ℂ ) )
19 12 17 18 sylancl ⊢ ( 𝜑 → ( 𝐶 –cn→ 𝐷 ) ⊆ ( 𝐶 –cn→ ℂ ) )
20 19 2 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 –cn→ ℂ ) )
21 1 20 cncfco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
22 16 21 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
23 cncfcdm ⊢ ( ( 𝐷 ⊆ ℂ ∧ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ 𝐷 ) )
24 12 22 23 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ 𝐷 ) )
25 10 24 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ 𝐷 ) )