| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . 4
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) | 
| 2 |  | cnmptk1p.c | . . . 4
⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) | 
| 3 |  | cnmptk1p.j | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 4 |  | cnmptk1p.k | . . . . . 6
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 5 |  | cnmptk1p.b | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) | 
| 6 |  | cnf2 23258 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶𝑌) | 
| 7 | 3, 4, 5, 6 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵):𝑋⟶𝑌) | 
| 8 | 7 | fvmptelcdm 7132 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑌) | 
| 9 | 2 | eleq1d 2825 | . . . . 5
⊢ (𝑦 = 𝐵 → (𝐴 ∈ 𝑍 ↔ 𝐶 ∈ 𝑍)) | 
| 10 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) | 
| 11 |  | cnmptk1p.l | . . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) | 
| 12 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘𝑍)) | 
| 13 |  | cnmptk1p.n | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
Comp) | 
| 14 |  | nllytop 23482 | . . . . . . . . . . 11
⊢ (𝐾 ∈ 𝑛-Locally Comp
→ 𝐾 ∈
Top) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 16 |  | topontop 22920 | . . . . . . . . . . 11
⊢ (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top) | 
| 17 | 11, 16 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ Top) | 
| 18 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾) | 
| 19 | 18 | xkotopon 23609 | . . . . . . . . . 10
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 20 | 15, 17, 19 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 21 |  | cnmptk1p.a | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) | 
| 22 |  | cnf2 23258 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) | 
| 23 | 3, 20, 21, 22 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) | 
| 24 | 23 | fvmptelcdm 7132 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) | 
| 25 |  | cnf2 23258 | . . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) | 
| 26 | 10, 12, 24, 25 | syl3anc 1372 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) | 
| 27 | 1 | fmpt 7129 | . . . . . 6
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ 𝑍 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) | 
| 28 | 26, 27 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) | 
| 29 | 9, 28, 8 | rspcdva 3622 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ 𝑍) | 
| 30 | 1, 2, 8, 29 | fvmptd3 7038 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵) = 𝐶) | 
| 31 | 30 | mpteq2dva 5241 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) | 
| 32 |  | eqid 2736 | . . . . 5
⊢ (𝐾 Cn 𝐿) = (𝐾 Cn 𝐿) | 
| 33 |  | toponuni 22921 | . . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) | 
| 34 | 4, 33 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝐾) | 
| 35 |  | mpoeq12 7507 | . . . . 5
⊢ (((𝐾 Cn 𝐿) = (𝐾 Cn 𝐿) ∧ 𝑌 = ∪ 𝐾) → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧))) | 
| 36 | 32, 34, 35 | sylancr 587 | . . . 4
⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧))) | 
| 37 |  | eqid 2736 | . . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 38 |  | eqid 2736 | . . . . . 6
⊢ (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) | 
| 39 | 37, 38 | xkofvcn 23693 | . . . . 5
⊢ ((𝐾 ∈ 𝑛-Locally Comp
∧ 𝐿 ∈ Top) →
(𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ↑ko 𝐾) ×t 𝐾) Cn 𝐿)) | 
| 40 | 13, 17, 39 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ↑ko 𝐾) ×t 𝐾) Cn 𝐿)) | 
| 41 | 36, 40 | eqeltrd 2840 | . . 3
⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ↑ko 𝐾) ×t 𝐾) Cn 𝐿)) | 
| 42 |  | fveq1 6904 | . . . 4
⊢ (𝑓 = (𝑦 ∈ 𝑌 ↦ 𝐴) → (𝑓‘𝑧) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧)) | 
| 43 |  | fveq2 6905 | . . . 4
⊢ (𝑧 = 𝐵 → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑧) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) | 
| 44 | 42, 43 | sylan9eq 2796 | . . 3
⊢ ((𝑓 = (𝑦 ∈ 𝑌 ↦ 𝐴) ∧ 𝑧 = 𝐵) → (𝑓‘𝑧) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) | 
| 45 | 3, 21, 5, 20, 4, 41, 44 | cnmpt12 23676 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) ∈ (𝐽 Cn 𝐿)) | 
| 46 | 31, 45 | eqeltrrd 2841 | 1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |