Step | Hyp | Ref
| Expression |
1 | | cnmptkk.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | cnmptkk.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘𝑍)) |
5 | | cnmptkk.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
6 | | topontop 20541 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
7 | 1, 6 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Top) |
8 | | cnmptkk.n |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿 ∈ 𝑛-Locally
Comp) |
9 | | nllytop 21086 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ 𝑛-Locally Comp
→ 𝐿 ∈
Top) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ Top) |
11 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾) |
12 | 11 | xkotopon 21213 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
13 | 7, 10, 12 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
14 | | cnmptkk.a |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
15 | | cnf2 20863 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
16 | 5, 13, 14, 15 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) |
18 | 17 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿) ↔ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
19 | 16, 18 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
20 | 19 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
21 | | cnf2 20863 |
. . . . . 6
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
22 | 2, 4, 20, 21 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
23 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) |
24 | 23 | fmpt 6289 |
. . . . 5
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ 𝑍 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
25 | 22, 24 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) |
26 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
27 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑍 ↦ 𝐵) = (𝑧 ∈ 𝑍 ↦ 𝐵)) |
28 | | cnmptkk.c |
. . . 4
⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) |
29 | 25, 26, 27, 28 | fmptcof 6304 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑦 ∈ 𝑌 ↦ 𝐶)) |
30 | 29 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶))) |
31 | | cnmptkk.b |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐽 Cn (𝑀 ^ko 𝐿))) |
32 | | cnmptkk.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) |
33 | | topontop 20541 |
. . . . 5
⊢ (𝑀 ∈ (TopOn‘𝑊) → 𝑀 ∈ Top) |
34 | 32, 33 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ Top) |
35 | | eqid 2610 |
. . . . 5
⊢ (𝑀 ^ko 𝐿) = (𝑀 ^ko 𝐿) |
36 | 35 | xkotopon 21213 |
. . . 4
⊢ ((𝐿 ∈ Top ∧ 𝑀 ∈ Top) → (𝑀 ^ko 𝐿) ∈ (TopOn‘(𝐿 Cn 𝑀))) |
37 | 10, 34, 36 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑀 ^ko 𝐿) ∈ (TopOn‘(𝐿 Cn 𝑀))) |
38 | | eqid 2610 |
. . . . 5
⊢ (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) |
39 | 38 | xkococn 21273 |
. . . 4
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ 𝑛-Locally Comp
∧ 𝑀 ∈ Top) →
(𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) ∈ (((𝑀 ^ko 𝐿) ×t (𝐿 ^ko 𝐾)) Cn (𝑀 ^ko 𝐾))) |
40 | 7, 8, 34, 39 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) ∈ (((𝑀 ^ko 𝐿) ×t (𝐿 ^ko 𝐾)) Cn (𝑀 ^ko 𝐾))) |
41 | | coeq1 5201 |
. . . 4
⊢ (𝑓 = (𝑧 ∈ 𝑍 ↦ 𝐵) → (𝑓 ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑔)) |
42 | | coeq2 5202 |
. . . 4
⊢ (𝑔 = (𝑦 ∈ 𝑌 ↦ 𝐴) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
43 | 41, 42 | sylan9eq 2664 |
. . 3
⊢ ((𝑓 = (𝑧 ∈ 𝑍 ↦ 𝐵) ∧ 𝑔 = (𝑦 ∈ 𝑌 ↦ 𝐴)) → (𝑓 ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) |
44 | 5, 31, 14, 37, 13, 40, 43 | cnmpt12 21280 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) ∈ (𝐽 Cn (𝑀 ^ko 𝐾))) |
45 | 30, 44 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ^ko 𝐾))) |