Step | Hyp | Ref
| Expression |
1 | | unieq 4880 |
. . . 4
β’ (π = π½ β βͺ π = βͺ
π½) |
2 | 1 | oveq2d 7377 |
. . 3
β’ (π = π½ β (βͺ π βpm βͺ π) =
(βͺ π βpm βͺ π½)) |
3 | | fveq2 6846 |
. . . . 5
β’ (π = π½ β (clsβπ) = (clsβπ½)) |
4 | 3 | fveq1d 6848 |
. . . 4
β’ (π = π½ β ((clsβπ)βdom π) = ((clsβπ½)βdom π)) |
5 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π½ β (neiβπ) = (neiβπ½)) |
6 | 5 | fveq1d 6848 |
. . . . . . . 8
β’ (π = π½ β ((neiβπ)β{π₯}) = ((neiβπ½)β{π₯})) |
7 | 6 | oveq1d 7376 |
. . . . . . 7
β’ (π = π½ β (((neiβπ)β{π₯}) βΎt dom π) = (((neiβπ½)β{π₯}) βΎt dom π)) |
8 | 7 | oveq2d 7377 |
. . . . . 6
β’ (π = π½ β (π fLimf (((neiβπ)β{π₯}) βΎt dom π)) = (π fLimf (((neiβπ½)β{π₯}) βΎt dom π))) |
9 | 8 | fveq1d 6848 |
. . . . 5
β’ (π = π½ β ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ) = ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)) |
10 | 9 | xpeq2d 5667 |
. . . 4
β’ (π = π½ β ({π₯} Γ ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ)) = ({π₯} Γ ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ))) |
11 | 4, 10 | iuneq12d 4986 |
. . 3
β’ (π = π½ β βͺ
π₯ β ((clsβπ)βdom π)({π₯} Γ ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ)) = βͺ
π₯ β ((clsβπ½)βdom π)({π₯} Γ ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ))) |
12 | 2, 11 | mpteq12dv 5200 |
. 2
β’ (π = π½ β (π β (βͺ π βpm βͺ π)
β¦ βͺ π₯ β ((clsβπ)βdom π)({π₯} Γ ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ))) = (π β (βͺ π βpm βͺ π½)
β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) |
13 | | unieq 4880 |
. . . 4
β’ (π = πΎ β βͺ π = βͺ
πΎ) |
14 | 13 | oveq1d 7376 |
. . 3
β’ (π = πΎ β (βͺ π βpm βͺ π½) =
(βͺ πΎ βpm βͺ π½)) |
15 | | oveq1 7368 |
. . . . . 6
β’ (π = πΎ β (π fLimf (((neiβπ½)β{π₯}) βΎt dom π)) = (πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))) |
16 | 15 | fveq1d 6848 |
. . . . 5
β’ (π = πΎ β ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ) = ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)) |
17 | 16 | xpeq2d 5667 |
. . . 4
β’ (π = πΎ β ({π₯} Γ ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)) = ({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ))) |
18 | 17 | iuneq2d 4987 |
. . 3
β’ (π = πΎ β βͺ
π₯ β ((clsβπ½)βdom π)({π₯} Γ ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)) = βͺ
π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ))) |
19 | 14, 18 | mpteq12dv 5200 |
. 2
β’ (π = πΎ β (π β (βͺ π βpm βͺ π½)
β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((π fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ))) = (π β (βͺ πΎ βpm βͺ π½)
β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) |
20 | | df-cnext 23434 |
. 2
β’ CnExt =
(π β Top, π β Top β¦ (π β (βͺ π
βpm βͺ π) β¦ βͺ
π₯ β ((clsβπ)βdom π)({π₯} Γ ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ)))) |
21 | | ovex 7394 |
. . 3
β’ (βͺ πΎ
βpm βͺ π½) β V |
22 | 21 | mptex 7177 |
. 2
β’ (π β (βͺ πΎ
βpm βͺ π½) β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ))) β V |
23 | 12, 19, 20, 22 | ovmpo 7519 |
1
β’ ((π½ β Top β§ πΎ β Top) β (π½CnExtπΎ) = (π β (βͺ πΎ βpm βͺ π½)
β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) |