| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) | 
| 2 |  | cnmptkp.c | . . . 4
⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) | 
| 3 |  | cnmptkp.b | . . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑌) | 
| 4 | 3 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑌) | 
| 5 | 2 | eleq1d 2826 | . . . . 5
⊢ (𝑦 = 𝐵 → (𝐴 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿)) | 
| 6 |  | cnmptk1.k | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 7 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) | 
| 8 |  | cnmptk1.l | . . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) | 
| 9 |  | topontop 22919 | . . . . . . . . . 10
⊢ (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top) | 
| 10 | 8, 9 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ Top) | 
| 11 | 10 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ Top) | 
| 12 |  | toptopon2 22924 | . . . . . . . 8
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) | 
| 13 | 11, 12 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿)) | 
| 14 |  | cnmptk1.j | . . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 15 |  | topontop 22919 | . . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) | 
| 16 | 6, 15 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 17 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝐿 ↑ko 𝐾) = (𝐿 ↑ko 𝐾) | 
| 18 | 17 | xkotopon 23608 | . . . . . . . . . 10
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 19 | 16, 10, 18 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) | 
| 20 |  | cnmptkp.a | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) | 
| 21 |  | cnf2 23257 | . . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ↑ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) | 
| 22 | 14, 19, 20, 21 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) | 
| 23 | 22 | fvmptelcdm 7133 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) | 
| 24 |  | cnf2 23257 | . . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶∪ 𝐿) | 
| 25 | 7, 13, 23, 24 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶∪ 𝐿) | 
| 26 | 1 | fmpt 7130 | . . . . . 6
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶∪ 𝐿) | 
| 27 | 25, 26 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿) | 
| 28 | 5, 27, 4 | rspcdva 3623 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ∪ 𝐿) | 
| 29 | 1, 2, 4, 28 | fvmptd3 7039 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵) = 𝐶) | 
| 30 | 29 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) | 
| 31 |  | toponuni 22920 | . . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) | 
| 32 | 6, 31 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝐾) | 
| 33 | 3, 32 | eleqtrd 2843 | . . . 4
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) | 
| 34 |  | eqid 2737 | . . . . 5
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 35 | 34 | xkopjcn 23664 | . . . 4
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝐵 ∈ ∪ 𝐾)
→ (𝑤 ∈ (𝐾 Cn 𝐿) ↦ (𝑤‘𝐵)) ∈ ((𝐿 ↑ko 𝐾) Cn 𝐿)) | 
| 36 | 16, 10, 33, 35 | syl3anc 1373 | . . 3
⊢ (𝜑 → (𝑤 ∈ (𝐾 Cn 𝐿) ↦ (𝑤‘𝐵)) ∈ ((𝐿 ↑ko 𝐾) Cn 𝐿)) | 
| 37 |  | fveq1 6905 | . . 3
⊢ (𝑤 = (𝑦 ∈ 𝑌 ↦ 𝐴) → (𝑤‘𝐵) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) | 
| 38 | 14, 20, 19, 36, 37 | cnmpt11 23671 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) ∈ (𝐽 Cn 𝐿)) | 
| 39 | 30, 38 | eqeltrrd 2842 | 1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |