Step | Hyp | Ref
| Expression |
1 | | cnmptkk.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
2 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | cnmptkk.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘𝑍)) |
5 | | cnmptkk.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
6 | | topontop 21837 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
7 | 1, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Top) |
8 | | cnmptkk.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ 𝑛-Locally
Comp) |
9 | | nllytop 22397 |
. . . . . . . . . 10
⊢ (𝐿 ∈ 𝑛-Locally Comp
→ 𝐿 ∈
Top) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ Top) |
11 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾) |
12 | 11 | xkotopon 22524 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
13 | 7, 10, 12 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
14 | | cnmptkk.a |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) |
15 | | cnf2 22173 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
16 | 5, 13, 14, 15 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
17 | 16 | fvmptelrn 6949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
18 | | cnf2 22173 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
19 | 2, 4, 17, 18 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
20 | | eqid 2738 |
. . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) |
21 | 20 | fmpt 6946 |
. . . . 5
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ 𝑍 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
22 | 19, 21 | sylibr 237 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) |
23 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
24 | | eqidd 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑍 ↦ 𝐵) = (𝑧 ∈ 𝑍 ↦ 𝐵)) |
25 | | cnmptkk.c |
. . . 4
⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) |
26 | 22, 23, 24, 25 | fmptcof 6964 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑦 ∈ 𝑌 ↦ 𝐶)) |
27 | 26 | mpteq2dva 5165 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶))) |
28 | | cnmptkk.b |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐿))) |
29 | | cnmptkk.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) |
30 | | topontop 21837 |
. . . . 5
⊢ (𝑀 ∈ (TopOn‘𝑊) → 𝑀 ∈ Top) |
31 | 29, 30 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Top) |
32 | | eqid 2738 |
. . . . 5
⊢ (𝑀 ↑ko 𝐿) = (𝑀 ↑ko 𝐿) |
33 | 32 | xkotopon 22524 |
. . . 4
⊢ ((𝐿 ∈ Top ∧ 𝑀 ∈ Top) → (𝑀 ↑ko 𝐿) ∈ (TopOn‘(𝐿 Cn 𝑀))) |
34 | 10, 31, 33 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑀 ↑ko 𝐿) ∈ (TopOn‘(𝐿 Cn 𝑀))) |
35 | | eqid 2738 |
. . . . 5
⊢ (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) |
36 | 35 | xkococn 22584 |
. . . 4
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ 𝑛-Locally Comp
∧ 𝑀 ∈ Top) →
(𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) ∈ (((𝑀 ↑ko 𝐿) ×t (𝐿 ↑ko 𝐾)) Cn (𝑀 ↑ko 𝐾))) |
37 | 7, 8, 31, 36 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) ∈ (((𝑀 ↑ko 𝐿) ×t (𝐿 ↑ko 𝐾)) Cn (𝑀 ↑ko 𝐾))) |
38 | | coeq1 5741 |
. . . 4
⊢ (𝑓 = (𝑧 ∈ 𝑍 ↦ 𝐵) → (𝑓 ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑔)) |
39 | | coeq2 5742 |
. . . 4
⊢ (𝑔 = (𝑦 ∈ 𝑌 ↦ 𝐴) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
40 | 38, 39 | sylan9eq 2799 |
. . 3
⊢ ((𝑓 = (𝑧 ∈ 𝑍 ↦ 𝐵) ∧ 𝑔 = (𝑦 ∈ 𝑌 ↦ 𝐴)) → (𝑓 ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
41 | 5, 28, 14, 34, 13, 37, 40 | cnmpt12 22591 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾))) |
42 | 27, 41 | eqeltrrd 2840 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾))) |