| 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 | . . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 6 |  | topontop 22919 | . . . . . . . . . 10
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) | 
| 7 | 1, 6 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 8 |  | cnmptkk.n | . . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ 𝑛-Locally
Comp) | 
| 9 |  | nllytop 23481 | . . . . . . . . . 10
⊢ (𝐿 ∈ 𝑛-Locally Comp
→ 𝐿 ∈
Top) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ Top) | 
| 11 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾) | 
| 12 | 11 | xkotopon 23608 | . . . . . . . . 9
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 13 | 7, 10, 12 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 14 |  | cnmptkk.a | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) | 
| 15 |  | cnf2 23257 | . . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) | 
| 16 | 5, 13, 14, 15 | syl3anc 1373 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) | 
| 17 | 16 | fvmptelcdm 7133 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) | 
| 18 |  | cnf2 23257 | . . . . . 6
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) | 
| 19 | 2, 4, 17, 18 | syl3anc 1373 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) | 
| 20 |  | eqid 2737 | . . . . . 6
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) | 
| 21 | 20 | fmpt 7130 | . . . . 5
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ 𝑍 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) | 
| 22 | 19, 21 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) | 
| 23 |  | eqidd 2738 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴)) | 
| 24 |  | eqidd 2738 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑧 ∈ 𝑍 ↦ 𝐵) = (𝑧 ∈ 𝑍 ↦ 𝐵)) | 
| 25 |  | cnmptkk.c | . . . 4
⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) | 
| 26 | 22, 23, 24, 25 | fmptcof 7150 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑦 ∈ 𝑌 ↦ 𝐶)) | 
| 27 | 26 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶))) | 
| 28 |  | cnmptkk.b | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐿))) | 
| 29 |  | cnmptkk.m | . . . . 5
⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) | 
| 30 |  | topontop 22919 | . . . . 5
⊢ (𝑀 ∈ (TopOn‘𝑊) → 𝑀 ∈ Top) | 
| 31 | 29, 30 | syl 17 | . . . 4
⊢ (𝜑 → 𝑀 ∈ Top) | 
| 32 |  | eqid 2737 | . . . . 5
⊢ (𝑀 ↑ko 𝐿) = (𝑀 ↑ko 𝐿) | 
| 33 | 32 | xkotopon 23608 | . . . 4
⊢ ((𝐿 ∈ Top ∧ 𝑀 ∈ Top) → (𝑀 ↑ko 𝐿) ∈ (TopOn‘(𝐿 Cn 𝑀))) | 
| 34 | 10, 31, 33 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑀 ↑ko 𝐿) ∈ (TopOn‘(𝐿 Cn 𝑀))) | 
| 35 |  | eqid 2737 | . . . . 5
⊢ (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ (𝐿 Cn 𝑀), 𝑔 ∈ (𝐾 Cn 𝐿) ↦ (𝑓 ∘ 𝑔)) | 
| 36 | 35 | xkococn 23668 | . . . 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 5868 | . . . 4
⊢ (𝑓 = (𝑧 ∈ 𝑍 ↦ 𝐵) → (𝑓 ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑔)) | 
| 39 |  | coeq2 5869 | . . . 4
⊢ (𝑔 = (𝑦 ∈ 𝑌 ↦ 𝐴) → ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) | 
| 40 | 38, 39 | sylan9eq 2797 | . . 3
⊢ ((𝑓 = (𝑧 ∈ 𝑍 ↦ 𝐵) ∧ 𝑔 = (𝑦 ∈ 𝑌 ↦ 𝐴)) → (𝑓 ∘ 𝑔) = ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) | 
| 41 | 5, 28, 14, 34, 13, 37, 40 | cnmpt12 23675 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑧 ∈ 𝑍 ↦ 𝐵) ∘ (𝑦 ∈ 𝑌 ↦ 𝐴))) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾))) | 
| 42 | 27, 41 | eqeltrrd 2842 | 1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾))) |