Metamath Proof Explorer

Theorem cnmpt1k

Description: The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses cnmptk1.j ⊢ φ → J ∈ TopOn ⁡ X
cnmptk1.k ⊢ φ → K ∈ TopOn ⁡ Y
cnmptk1.l ⊢ φ → L ∈ TopOn ⁡ Z
cnmpt1k.m ⊢ φ → M ∈ TopOn ⁡ W
cnmpt1k.a ⊢ φ → x ∈ X ⟼ A ∈ J Cn L
cnmpt1k.b ⊢ φ → y ∈ Y ⟼ z ∈ Z ⟼ B ∈ K Cn M ^ ko L
cnmpt1k.c ⊢ z = A → B = C
Assertion cnmpt1k ⊢ φ → y ∈ Y ⟼ x ∈ X ⟼ C ∈ K Cn M ^ ko J

Proof

Step Hyp Ref Expression
1 cnmptk1.j ⊢ φ → J ∈ TopOn ⁡ X
2 cnmptk1.k ⊢ φ → K ∈ TopOn ⁡ Y
3 cnmptk1.l ⊢ φ → L ∈ TopOn ⁡ Z
4 cnmpt1k.m ⊢ φ → M ∈ TopOn ⁡ W
5 cnmpt1k.a ⊢ φ → x ∈ X ⟼ A ∈ J Cn L
6 cnmpt1k.b ⊢ φ → y ∈ Y ⟼ z ∈ Z ⟼ B ∈ K Cn M ^ ko L
7 cnmpt1k.c ⊢ z = A → B = C
8 cnf2 ⊢ J ∈ TopOn ⁡ X ∧ L ∈ TopOn ⁡ Z ∧ x ∈ X ⟼ A ∈ J Cn L → x ∈ X ⟼ A : X ⟶ Z
9 1 3 5 8 syl3anc ⊢ φ → x ∈ X ⟼ A : X ⟶ Z
10 eqid ⊢ x ∈ X ⟼ A = x ∈ X ⟼ A
11 10 fmpt ⊢ ∀ x ∈ X A ∈ Z ↔ x ∈ X ⟼ A : X ⟶ Z
12 9 11 sylibr ⊢ φ → ∀ x ∈ X A ∈ Z
13 12 adantr ⊢ φ ∧ y ∈ Y → ∀ x ∈ X A ∈ Z
14 eqidd ⊢ φ ∧ y ∈ Y → x ∈ X ⟼ A = x ∈ X ⟼ A
15 eqidd ⊢ φ ∧ y ∈ Y → z ∈ Z ⟼ B = z ∈ Z ⟼ B
16 13 14 15 7 fmptcof ⊢ φ ∧ y ∈ Y → z ∈ Z ⟼ B ∘ x ∈ X ⟼ A = x ∈ X ⟼ C
17 16 mpteq2dva ⊢ φ → y ∈ Y ⟼ z ∈ Z ⟼ B ∘ x ∈ X ⟼ A = y ∈ Y ⟼ x ∈ X ⟼ C
18 topontop ⊢ L ∈ TopOn ⁡ Z → L ∈ Top
19 3 18 syl ⊢ φ → L ∈ Top
20 topontop ⊢ M ∈ TopOn ⁡ W → M ∈ Top
21 4 20 syl ⊢ φ → M ∈ Top
22 eqid ⊢ M ^ ko L = M ^ ko L
23 22 xkotopon ⊢ L ∈ Top ∧ M ∈ Top → M ^ ko L ∈ TopOn ⁡ L Cn M
24 19 21 23 syl2anc ⊢ φ → M ^ ko L ∈ TopOn ⁡ L Cn M
25 21 5 xkoco1cn ⊢ φ → w ∈ L Cn M ⟼ w ∘ x ∈ X ⟼ A ∈ M ^ ko L Cn M ^ ko J
26 coeq1 ⊢ w = z ∈ Z ⟼ B → w ∘ x ∈ X ⟼ A = z ∈ Z ⟼ B ∘ x ∈ X ⟼ A
27 2 6 24 25 26 cnmpt11 ⊢ φ → y ∈ Y ⟼ z ∈ Z ⟼ B ∘ x ∈ X ⟼ A ∈ K Cn M ^ ko J
28 17 27 eqeltrrd ⊢ φ → y ∈ Y ⟼ x ∈ X ⟼ C ∈ K Cn M ^ ko J