Metamath Proof Explorer

Theorem cnmpt22f

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
cnmpt2t.b ⊢ φ → x ∈ X , y ∈ Y ⟼ B ∈ J × t K Cn M
cnmpt22f.f ⊢ φ → F ∈ L × t M Cn N
Assertion cnmpt22f ⊢ φ → x ∈ X , y ∈ Y ⟼ A F B ∈ J × t K Cn N

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 cnmpt2t.b ⊢ φ → x ∈ X , y ∈ Y ⟼ B ∈ J × t K Cn M
5 cnmpt22f.f ⊢ φ → F ∈ L × t M Cn N
6 cntop2 ⊢ x ∈ X , y ∈ Y ⟼ A ∈ J × t K Cn L → L ∈ Top
7 3 6 syl ⊢ φ → L ∈ Top
8 toptopon2 ⊢ L ∈ Top ↔ L ∈ TopOn ⁡ ⋃ L
9 7 8 sylib ⊢ φ → L ∈ TopOn ⁡ ⋃ L
10 cntop2 ⊢ x ∈ X , y ∈ Y ⟼ B ∈ J × t K Cn M → M ∈ Top
11 4 10 syl ⊢ φ → M ∈ Top
12 toptopon2 ⊢ M ∈ Top ↔ M ∈ TopOn ⁡ ⋃ M
13 11 12 sylib ⊢ φ → M ∈ TopOn ⁡ ⋃ M
14 txtopon ⊢ L ∈ TopOn ⁡ ⋃ L ∧ M ∈ TopOn ⁡ ⋃ M → L × t M ∈ TopOn ⁡ ⋃ L × ⋃ M
15 9 13 14 syl2anc ⊢ φ → L × t M ∈ TopOn ⁡ ⋃ L × ⋃ M
16 cntop2 ⊢ F ∈ L × t M Cn N → N ∈ Top
17 5 16 syl ⊢ φ → N ∈ Top
18 toptopon2 ⊢ N ∈ Top ↔ N ∈ TopOn ⁡ ⋃ N
19 17 18 sylib ⊢ φ → N ∈ TopOn ⁡ ⋃ N
20 cnf2 ⊢ L × t M ∈ TopOn ⁡ ⋃ L × ⋃ M ∧ N ∈ TopOn ⁡ ⋃ N ∧ F ∈ L × t M Cn N → F : ⋃ L × ⋃ M ⟶ ⋃ N
21 15 19 5 20 syl3anc ⊢ φ → F : ⋃ L × ⋃ M ⟶ ⋃ N
22 21 ffnd ⊢ φ → F Fn ⋃ L × ⋃ M
23 fnov ⊢ F Fn ⋃ L × ⋃ M ↔ F = z ∈ ⋃ L , w ∈ ⋃ M ⟼ z F w
24 22 23 sylib ⊢ φ → F = z ∈ ⋃ L , w ∈ ⋃ M ⟼ z F w
25 24 5 eqeltrrd ⊢ φ → z ∈ ⋃ L , w ∈ ⋃ M ⟼ z F w ∈ L × t M Cn N
26 oveq12 ⊢ z = A ∧ w = B → z F w = A F B
27 1 2 3 4 9 13 25 26 cnmpt22 ⊢ φ → x ∈ X , y ∈ Y ⟼ A F B ∈ J × t K Cn N