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

Metamath Proof Explorer

Theorem cncfcompt2

Description: Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses cncfcompt2.xph ⊢ Ⅎ 𝑥 𝜑
cncfcompt2.ab ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐵 ) )
cncfcompt2.cd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∈ ( 𝐶 –cn→ 𝐸 ) )
cncfcompt2.bc ⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
cncfcompt2.st ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
Assertion cncfcompt2 ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ∈ ( 𝐴 –cn→ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 cncfcompt2.xph ⊢ Ⅎ 𝑥 𝜑
2 cncfcompt2.ab ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐵 ) )
3 cncfcompt2.cd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∈ ( 𝐶 –cn→ 𝐸 ) )
4 cncfcompt2.bc ⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
5 cncfcompt2.st ⊢ ( 𝑦 = 𝑅 → 𝑆 = 𝑇 )
6 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ⊆ 𝐶 )
7 cncff ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 )
8 2 7 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ 𝐵 )
9 8 fvmptelcdm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐵 )
10 6 9 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ 𝐶 )
11 10 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑅 ∈ 𝐶 ) )
12 1 11 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ 𝐶 )
13 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) = ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) )
15 12 13 14 5 fmptcof ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) = ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) )
16 15 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) = ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) )
17 cncfrss ⊢ ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∈ ( 𝐶 –cn→ 𝐸 ) → 𝐶 ⊆ ℂ )
18 3 17 syl ⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
19 cncfss ⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) ⊆ ( 𝐴 –cn→ 𝐶 ) )
20 4 18 19 syl2anc ⊢ ( 𝜑 → ( 𝐴 –cn→ 𝐵 ) ⊆ ( 𝐴 –cn→ 𝐶 ) )
21 20 2 sseldd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( 𝐴 –cn→ 𝐶 ) )
22 21 3 cncfco ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐶 ↦ 𝑆 ) ∘ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) ∈ ( 𝐴 –cn→ 𝐸 ) )
23 16 22 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑇 ) ∈ ( 𝐴 –cn→ 𝐸 ) )