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

Metamath Proof Explorer

Theorem cnmpt11f

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmptid.j ⊢ φ → J ∈ TopOn ⁡ X
cnmpt11.a ⊢ φ → x ∈ X ⟼ A ∈ J Cn K
cnmpt11f.f ⊢ φ → F ∈ K Cn L
Assertion cnmpt11f ⊢ φ → x ∈ X ⟼ F ⁡ A ∈ J Cn L

Proof

Step Hyp Ref Expression
1 cnmptid.j ⊢ φ → J ∈ TopOn ⁡ X
2 cnmpt11.a ⊢ φ → x ∈ X ⟼ A ∈ J Cn K
3 cnmpt11f.f ⊢ φ → F ∈ K Cn L
4 cntop2 ⊢ x ∈ X ⟼ A ∈ J Cn K → K ∈ Top
5 2 4 syl ⊢ φ → K ∈ Top
6 toptopon2 ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ ⋃ K
7 5 6 sylib ⊢ φ → K ∈ TopOn ⁡ ⋃ K
8 eqid ⊢ ⋃ K = ⋃ K
9 eqid ⊢ ⋃ L = ⋃ L
10 8 9 cnf ⊢ F ∈ K Cn L → F : ⋃ K ⟶ ⋃ L
11 3 10 syl ⊢ φ → F : ⋃ K ⟶ ⋃ L
12 11 feqmptd ⊢ φ → F = y ∈ ⋃ K ⟼ F ⁡ y
13 12 3 eqeltrrd ⊢ φ → y ∈ ⋃ K ⟼ F ⁡ y ∈ K Cn L
14 fveq2 ⊢ y = A → F ⁡ y = F ⁡ A
15 1 2 7 13 14 cnmpt11 ⊢ φ → x ∈ X ⟼ F ⁡ A ∈ J Cn L