Metamath Proof Explorer

Theorem cnmpt11

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
cnmpt11.k ⊢ φ → K ∈ TopOn ⁡ Y
cnmpt11.b ⊢ φ → y ∈ Y ⟼ B ∈ K Cn L
cnmpt11.c ⊢ y = A → B = C
Assertion cnmpt11 ⊢ φ → x ∈ X ⟼ C ∈ J Cn L

Proof

Step Hyp Ref Expression
1 cnmptid.j ⊢ φ → J ∈ TopOn ⁡ X
2 cnmpt11.a ⊢ φ → x ∈ X ⟼ A ∈ J Cn K
3 cnmpt11.k ⊢ φ → K ∈ TopOn ⁡ Y
4 cnmpt11.b ⊢ φ → y ∈ Y ⟼ B ∈ K Cn L
5 cnmpt11.c ⊢ y = A → B = C
6 simpr ⊢ φ ∧ x ∈ X → x ∈ X
7 cnf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ X ⟼ A ∈ J Cn K → x ∈ X ⟼ A : X ⟶ Y
8 1 3 2 7 syl3anc ⊢ φ → x ∈ X ⟼ A : X ⟶ Y
9 8 fvmptelrn ⊢ φ ∧ x ∈ X → A ∈ Y
10 eqid ⊢ x ∈ X ⟼ A = x ∈ X ⟼ A
11 10 fvmpt2 ⊢ x ∈ X ∧ A ∈ Y → x ∈ X ⟼ A ⁡ x = A
12 6 9 11 syl2anc ⊢ φ ∧ x ∈ X → x ∈ X ⟼ A ⁡ x = A
13 12 fveq2d ⊢ φ ∧ x ∈ X → y ∈ Y ⟼ B ⁡ x ∈ X ⟼ A ⁡ x = y ∈ Y ⟼ B ⁡ A
14 eqid ⊢ y ∈ Y ⟼ B = y ∈ Y ⟼ B
15 5 eleq1d ⊢ y = A → B ∈ ⋃ L ↔ C ∈ ⋃ L
16 cntop2 ⊢ y ∈ Y ⟼ B ∈ K Cn L → L ∈ Top
17 4 16 syl ⊢ φ → L ∈ Top
18 toptopon2 ⊢ L ∈ Top ↔ L ∈ TopOn ⁡ ⋃ L
19 17 18 sylib ⊢ φ → L ∈ TopOn ⁡ ⋃ L
20 cnf2 ⊢ K ∈ TopOn ⁡ Y ∧ L ∈ TopOn ⁡ ⋃ L ∧ y ∈ Y ⟼ B ∈ K Cn L → y ∈ Y ⟼ B : Y ⟶ ⋃ L
21 3 19 4 20 syl3anc ⊢ φ → y ∈ Y ⟼ B : Y ⟶ ⋃ L
22 14 fmpt ⊢ ∀ y ∈ Y B ∈ ⋃ L ↔ y ∈ Y ⟼ B : Y ⟶ ⋃ L
23 21 22 sylibr ⊢ φ → ∀ y ∈ Y B ∈ ⋃ L
24 23 adantr ⊢ φ ∧ x ∈ X → ∀ y ∈ Y B ∈ ⋃ L
25 15 24 9 rspcdva ⊢ φ ∧ x ∈ X → C ∈ ⋃ L
26 14 5 9 25 fvmptd3 ⊢ φ ∧ x ∈ X → y ∈ Y ⟼ B ⁡ A = C
27 13 26 eqtrd ⊢ φ ∧ x ∈ X → y ∈ Y ⟼ B ⁡ x ∈ X ⟼ A ⁡ x = C
28 fvco3 ⊢ x ∈ X ⟼ A : X ⟶ Y ∧ x ∈ X → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = y ∈ Y ⟼ B ⁡ x ∈ X ⟼ A ⁡ x
29 8 28 sylan ⊢ φ ∧ x ∈ X → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = y ∈ Y ⟼ B ⁡ x ∈ X ⟼ A ⁡ x
30 eqid ⊢ x ∈ X ⟼ C = x ∈ X ⟼ C
31 30 fvmpt2 ⊢ x ∈ X ∧ C ∈ ⋃ L → x ∈ X ⟼ C ⁡ x = C
32 6 25 31 syl2anc ⊢ φ ∧ x ∈ X → x ∈ X ⟼ C ⁡ x = C
33 27 29 32 3eqtr4d ⊢ φ ∧ x ∈ X → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = x ∈ X ⟼ C ⁡ x
34 33 ralrimiva ⊢ φ → ∀ x ∈ X y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = x ∈ X ⟼ C ⁡ x
35 nfv ⊢ Ⅎ z y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = x ∈ X ⟼ C ⁡ x
36 nfcv ⊢ Ⅎ _ x y ∈ Y ⟼ B
37 nfmpt1 ⊢ Ⅎ _ x x ∈ X ⟼ A
38 36 37 nfco ⊢ Ⅎ _ x y ∈ Y ⟼ B ∘ x ∈ X ⟼ A
39 nfcv ⊢ Ⅎ _ x z
40 38 39 nffv ⊢ Ⅎ _ x y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z
41 nfmpt1 ⊢ Ⅎ _ x x ∈ X ⟼ C
42 41 39 nffv ⊢ Ⅎ _ x x ∈ X ⟼ C ⁡ z
43 40 42 nfeq ⊢ Ⅎ x y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z = x ∈ X ⟼ C ⁡ z
44 fveq2 ⊢ x = z → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z
45 fveq2 ⊢ x = z → x ∈ X ⟼ C ⁡ x = x ∈ X ⟼ C ⁡ z
46 44 45 eqeq12d ⊢ x = z → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = x ∈ X ⟼ C ⁡ x ↔ y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z = x ∈ X ⟼ C ⁡ z
47 35 43 46 cbvralw ⊢ ∀ x ∈ X y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ x = x ∈ X ⟼ C ⁡ x ↔ ∀ z ∈ X y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z = x ∈ X ⟼ C ⁡ z
48 34 47 sylib ⊢ φ → ∀ z ∈ X y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z = x ∈ X ⟼ C ⁡ z
49 fco ⊢ y ∈ Y ⟼ B : Y ⟶ ⋃ L ∧ x ∈ X ⟼ A : X ⟶ Y → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A : X ⟶ ⋃ L
50 21 8 49 syl2anc ⊢ φ → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A : X ⟶ ⋃ L
51 50 ffnd ⊢ φ → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A Fn X
52 25 fmpttd ⊢ φ → x ∈ X ⟼ C : X ⟶ ⋃ L
53 52 ffnd ⊢ φ → x ∈ X ⟼ C Fn X
54 eqfnfv ⊢ y ∈ Y ⟼ B ∘ x ∈ X ⟼ A Fn X ∧ x ∈ X ⟼ C Fn X → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A = x ∈ X ⟼ C ↔ ∀ z ∈ X y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z = x ∈ X ⟼ C ⁡ z
55 51 53 54 syl2anc ⊢ φ → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A = x ∈ X ⟼ C ↔ ∀ z ∈ X y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ⁡ z = x ∈ X ⟼ C ⁡ z
56 48 55 mpbird ⊢ φ → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A = x ∈ X ⟼ C
57 cnco ⊢ x ∈ X ⟼ A ∈ J Cn K ∧ y ∈ Y ⟼ B ∈ K Cn L → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ∈ J Cn L
58 2 4 57 syl2anc ⊢ φ → y ∈ Y ⟼ B ∘ x ∈ X ⟼ A ∈ J Cn L
59 56 58 eqeltrrd ⊢ φ → x ∈ X ⟼ C ∈ J Cn L