Step | Hyp | Ref
| Expression |
1 | | nffvmpt1 6111 |
. . . . 5
⊢
Ⅎ𝑥((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) |
2 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑥𝑘 |
3 | 1, 2 | nffv 6110 |
. . . 4
⊢
Ⅎ𝑥(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘) |
4 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦𝑋 |
5 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑦(𝑦 ∈ 𝑌 ↦ 𝐴) |
6 | 4, 5 | nfmpt 4674 |
. . . . . 6
⊢
Ⅎ𝑦(𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) |
7 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑦𝑤 |
8 | 6, 7 | nffv 6110 |
. . . . 5
⊢
Ⅎ𝑦((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) |
9 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦𝑘 |
10 | 8, 9 | nffv 6110 |
. . . 4
⊢
Ⅎ𝑦(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘) |
11 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑤(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) |
12 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑘(((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) |
13 | | fveq2 6103 |
. . . . . 6
⊢ (𝑤 = 𝑥 → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)) |
14 | 13 | fveq1d 6105 |
. . . . 5
⊢ (𝑤 = 𝑥 → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑘)) |
15 | | fveq2 6103 |
. . . . 5
⊢ (𝑘 = 𝑦 → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑘) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)) |
16 | 14, 15 | sylan9eq 2664 |
. . . 4
⊢ ((𝑤 = 𝑥 ∧ 𝑘 = 𝑦) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)) |
17 | 3, 10, 11, 12, 16 | cbvmpt2 6632 |
. . 3
⊢ (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)) |
18 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
19 | | cnmptk1p.j |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
20 | | cnmptk1p.n |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally
Comp) |
21 | | nllytop 21086 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ 𝑛-Locally Comp
→ 𝐾 ∈
Top) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ Top) |
23 | | cnmptk1p.l |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) |
24 | | topontop 20541 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ (TopOn‘𝑍) → 𝐿 ∈ Top) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ Top) |
26 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ^ko 𝐾) = (𝐿 ^ko 𝐾) |
27 | 26 | xkotopon 21213 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Top ∧ 𝐿 ∈ Top) → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
28 | 22, 25, 27 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿))) |
29 | | cnmptk2.a |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
30 | | cnf2 20863 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐿 ^ko 𝐾) ∈ (TopOn‘(𝐾 Cn 𝐿)) ∧ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
31 | 19, 28, 29, 30 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
32 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) |
33 | 32 | fmpt 6289 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿) ↔ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)):𝑋⟶(𝐾 Cn 𝐿)) |
34 | 31, 33 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
35 | 34 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
36 | 35 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) |
37 | 32 | fvmpt2 6200 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
38 | 18, 36, 37 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥) = (𝑦 ∈ 𝑌 ↦ 𝐴)) |
39 | 38 | fveq1d 6105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) = ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑦)) |
40 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) |
41 | | cnmptk1p.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
42 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈ (TopOn‘𝑌)) |
43 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐿 ∈ (TopOn‘𝑍)) |
44 | | cnf2 20863 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (TopOn‘𝑍) ∧ (𝑦 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
45 | 42, 43, 35, 44 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
46 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝑌 ↦ 𝐴) = (𝑦 ∈ 𝑌 ↦ 𝐴) |
47 | 46 | fmpt 6289 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑌 𝐴 ∈ 𝑍 ↔ (𝑦 ∈ 𝑌 ↦ 𝐴):𝑌⟶𝑍) |
48 | 45, 47 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑌 𝐴 ∈ 𝑍) |
49 | 48 | r19.21bi 2916 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → 𝐴 ∈ 𝑍) |
50 | 46 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝑌 ∧ 𝐴 ∈ 𝑍) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑦) = 𝐴) |
51 | 40, 49, 50 | syl2anc 691 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → ((𝑦 ∈ 𝑌 ↦ 𝐴)‘𝑦) = 𝐴) |
52 | 39, 51 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑌) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) = 𝐴) |
53 | 52 | 3impa 1251 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦) = 𝐴) |
54 | 53 | mpt2eq3dva 6617 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑥)‘𝑦)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) |
55 | 17, 54 | syl5eq 2656 |
. 2
⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴)) |
56 | 19, 41 | cnmpt1st 21281 |
. . . 4
⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ 𝑤) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
57 | 19, 41, 56, 29 | cnmpt21f 21285 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ^ko 𝐾))) |
58 | 19, 41 | cnmpt2nd 21282 |
. . 3
⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ 𝑘) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
59 | | eqid 2610 |
. . . . 5
⊢ (𝐾 Cn 𝐿) = (𝐾 Cn 𝐿) |
60 | | toponuni 20542 |
. . . . . 6
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) |
61 | 41, 60 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑌 = ∪ 𝐾) |
62 | | mpt2eq12 6613 |
. . . . 5
⊢ (((𝐾 Cn 𝐿) = (𝐾 Cn 𝐿) ∧ 𝑌 = ∪ 𝐾) → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧))) |
63 | 59, 61, 62 | sylancr 694 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧))) |
64 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐾 =
∪ 𝐾 |
65 | | eqid 2610 |
. . . . . 6
⊢ (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) = (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) |
66 | 64, 65 | xkofvcn 21297 |
. . . . 5
⊢ ((𝐾 ∈ 𝑛-Locally Comp
∧ 𝐿 ∈ Top) →
(𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ^ko 𝐾) ×t 𝐾) Cn 𝐿)) |
67 | 20, 25, 66 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ ∪ 𝐾 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ^ko 𝐾) ×t 𝐾) Cn 𝐿)) |
68 | 63, 67 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (𝑓 ∈ (𝐾 Cn 𝐿), 𝑧 ∈ 𝑌 ↦ (𝑓‘𝑧)) ∈ (((𝐿 ^ko 𝐾) ×t 𝐾) Cn 𝐿)) |
69 | | fveq1 6102 |
. . . 4
⊢ (𝑓 = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) → (𝑓‘𝑧) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑧)) |
70 | | fveq2 6103 |
. . . 4
⊢ (𝑧 = 𝑘 → (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑧) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) |
71 | 69, 70 | sylan9eq 2664 |
. . 3
⊢ ((𝑓 = ((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤) ∧ 𝑧 = 𝑘) → (𝑓‘𝑧) = (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) |
72 | 19, 41, 57, 58, 28, 41, 68, 71 | cnmpt22 21287 |
. 2
⊢ (𝜑 → (𝑤 ∈ 𝑋, 𝑘 ∈ 𝑌 ↦ (((𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴))‘𝑤)‘𝑘)) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |
73 | 55, 72 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) |