Step | Hyp | Ref
| Expression |
1 | | unieq 4380 |
. . . 4
⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪
𝐽) |
2 | 1 | oveq2d 6565 |
. . 3
⊢ (𝑗 = 𝐽 → (∪ 𝑘 ↑pm
∪ 𝑗) = (∪ 𝑘 ↑pm
∪ 𝐽)) |
3 | | fveq2 6103 |
. . . . 5
⊢ (𝑗 = 𝐽 → (cls‘𝑗) = (cls‘𝐽)) |
4 | 3 | fveq1d 6105 |
. . . 4
⊢ (𝑗 = 𝐽 → ((cls‘𝑗)‘dom 𝑓) = ((cls‘𝐽)‘dom 𝑓)) |
5 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = 𝐽 → (nei‘𝑗) = (nei‘𝐽)) |
6 | 5 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑗 = 𝐽 → ((nei‘𝑗)‘{𝑥}) = ((nei‘𝐽)‘{𝑥})) |
7 | 6 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑗 = 𝐽 → (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓) = (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓)) |
8 | 7 | oveq2d 6565 |
. . . . . 6
⊢ (𝑗 = 𝐽 → (𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓)) = (𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))) |
9 | 8 | fveq1d 6105 |
. . . . 5
⊢ (𝑗 = 𝐽 → ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓) = ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) |
10 | 9 | xpeq2d 5063 |
. . . 4
⊢ (𝑗 = 𝐽 → ({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) = ({𝑥} × ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) |
11 | 4, 10 | iuneq12d 4482 |
. . 3
⊢ (𝑗 = 𝐽 → ∪
𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) = ∪
𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) |
12 | 2, 11 | mpteq12dv 4663 |
. 2
⊢ (𝑗 = 𝐽 → (𝑓 ∈ (∪ 𝑘 ↑pm
∪ 𝑗) ↦ ∪
𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) = (𝑓 ∈ (∪ 𝑘 ↑pm
∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) |
13 | | unieq 4380 |
. . . 4
⊢ (𝑘 = 𝐾 → ∪ 𝑘 = ∪
𝐾) |
14 | 13 | oveq1d 6564 |
. . 3
⊢ (𝑘 = 𝐾 → (∪ 𝑘 ↑pm
∪ 𝐽) = (∪ 𝐾 ↑pm
∪ 𝐽)) |
15 | | oveq1 6556 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓)) = (𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))) |
16 | 15 | fveq1d 6105 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓) = ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) |
17 | 16 | xpeq2d 5063 |
. . . 4
⊢ (𝑘 = 𝐾 → ({𝑥} × ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) = ({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) |
18 | 17 | iuneq2d 4483 |
. . 3
⊢ (𝑘 = 𝐾 → ∪
𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)) = ∪
𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) |
19 | 14, 18 | mpteq12dv 4663 |
. 2
⊢ (𝑘 = 𝐾 → (𝑓 ∈ (∪ 𝑘 ↑pm
∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) = (𝑓 ∈ (∪ 𝐾 ↑pm
∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) |
20 | | df-cnext 21674 |
. 2
⊢ CnExt =
(𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘
↑pm ∪ 𝑗) ↦ ∪
𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) |
21 | | ovex 6577 |
. . 3
⊢ (∪ 𝐾
↑pm ∪ 𝐽) ∈ V |
22 | 21 | mptex 6390 |
. 2
⊢ (𝑓 ∈ (∪ 𝐾
↑pm ∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))) ∈ V |
23 | 12, 19, 20, 22 | ovmpt2 6694 |
1
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽CnExt𝐾) = (𝑓 ∈ (∪ 𝐾 ↑pm
∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) |