Step | Hyp | Ref
| Expression |
1 | | cnmptkp.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑌) |
3 | | cnmptk1.k |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
4 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
5 | | cnmptk1.l |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
6 | | topontop 20541 |
. . . . . . . . . 10
⊢ (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ Top) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ Top) |
9 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ 𝐿 =
∪ 𝐿 |
10 | 9 | toptopon 20548 |
. . . . . . . 8
⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿)) |
11 | 8, 10 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘∪ 𝐿)) |
12 | | cnmptk1.j |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
13 | | topontop 20541 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ Top) |
15 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾) |
16 | 15 | xkotopon 21213 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
17 | 14, 7, 16 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
18 | | cnmptkp.a |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
19 | | cnf2 20863 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
20 | 12, 17, 18, 19 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
21 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) |
22 | 21 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿) ↔ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
23 | 20, 22 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
24 | 23 | r19.21bi 2916 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
25 | | cnf2 20863 |
. . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘∪ 𝐿)
∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶∪ 𝐿) |
26 | 4, 11, 24, 25 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶∪ 𝐿) |
27 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) |
28 | 27 | fmpt 6289 |
. . . . . 6
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ ∪ 𝐿 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶∪ 𝐿) |
29 | 26, 28 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿) |
30 | | cnmptkp.c |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) |
31 | 30 | eleq1d 2672 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 ∈ ∪ 𝐿 ↔ 𝐶 ∈ ∪ 𝐿)) |
32 | 31 | rspcv 3278 |
. . . . 5
⊢ (𝐵 ∈ 𝑌 → (∀𝑦 ∈ 𝑌 𝐴 ∈ ∪ 𝐿 → 𝐶 ∈ ∪ 𝐿)) |
33 | 2, 29, 32 | sylc 63 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ ∪ 𝐿) |
34 | 30, 27 | fvmptg 6189 |
. . . 4
⊢ ((𝐵 ∈ 𝑌 ∧ 𝐶 ∈ ∪ 𝐿) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵) = 𝐶) |
35 | 2, 33, 34 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵) = 𝐶) |
36 | 35 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) = (𝑥 ∈ 𝑋 ↦ 𝐶)) |
37 | | toponuni 20542 |
. . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) |
38 | 3, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝐾) |
39 | 1, 38 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐾) |
40 | | eqid 2610 |
. . . . 5
⊢ ∪ 𝐾 =
∪ 𝐾 |
41 | 40 | xkopjcn 21269 |
. . . 4
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top ∧ 𝐵 ∈ ∪ 𝐾)
→ (𝑤 ∈ (𝐾 Cn 𝐿) ↦ (𝑤‘𝐵)) ∈ ((𝐿 ^ko 𝐾) Cn 𝐿)) |
42 | 14, 7, 39, 41 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝑤 ∈ (𝐾 Cn 𝐿) ↦ (𝑤‘𝐵)) ∈ ((𝐿 ^ko 𝐾) Cn 𝐿)) |
43 | | fveq1 6102 |
. . 3
⊢ (𝑤 = (𝑦 ∈ 𝑌 ↦ 𝐴) → (𝑤‘𝐵) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) |
44 | 12, 18, 17, 42, 43 | cnmpt11 21276 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝐵)) ∈ (𝐽 Cn 𝐿)) |
45 | 36, 44 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) |