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

Metamath Proof Explorer

Theorem cnmpt21f

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 cnmpt21.j ⊢ φ → J ∈ TopOn ⁡ X
cnmpt21.k ⊢ φ → K ∈ TopOn ⁡ Y
cnmpt21.a ⊢ φ → x ∈ X , y ∈ Y ⟼ A ∈ J × t K Cn L
cnmpt21f.f ⊢ φ → F ∈ L Cn M
Assertion cnmpt21f ⊢ φ → x ∈ X , y ∈ Y ⟼ F ⁡ A ∈ J × t K Cn M

Proof

Step Hyp Ref Expression
1 cnmpt21.j ⊢ φ → J ∈ TopOn ⁡ X
2 cnmpt21.k ⊢ φ → K ∈ TopOn ⁡ Y
3 cnmpt21.a ⊢ φ → x ∈ X , y ∈ Y ⟼ A ∈ J × t K Cn L
4 cnmpt21f.f ⊢ φ → F ∈ L Cn M
5 cntop1 ⊢ F ∈ L Cn M → L ∈ Top
6 4 5 syl ⊢ φ → L ∈ Top
7 toptopon2 ⊢ L ∈ Top ↔ L ∈ TopOn ⁡ ⋃ L
8 6 7 sylib ⊢ φ → L ∈ TopOn ⁡ ⋃ L
9 eqid ⊢ ⋃ L = ⋃ L
10 eqid ⊢ ⋃ M = ⋃ M
11 9 10 cnf ⊢ F ∈ L Cn M → F : ⋃ L ⟶ ⋃ M
12 4 11 syl ⊢ φ → F : ⋃ L ⟶ ⋃ M
13 12 feqmptd ⊢ φ → F = z ∈ ⋃ L ⟼ F ⁡ z
14 13 4 eqeltrrd ⊢ φ → z ∈ ⋃ L ⟼ F ⁡ z ∈ L Cn M
15 fveq2 ⊢ z = A → F ⁡ z = F ⁡ A
16 1 2 3 8 14 15 cnmpt21 ⊢ φ → x ∈ X , y ∈ Y ⟼ F ⁡ A ∈ J × t K Cn M