Step | Hyp | Ref
| Expression |
1 | | topontop 22285 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | | id 22 |
. . . . 5
β’ (π = π½ β π = π½) |
3 | | unieq 4880 |
. . . . . 6
β’ (π = π½ β βͺ π = βͺ
π½) |
4 | | rabeq 3420 |
. . . . . 6
β’ (π = π½ β {π¦ β π β£ π₯ β π¦} = {π¦ β π½ β£ π₯ β π¦}) |
5 | 3, 4 | mpteq12dv 5200 |
. . . . 5
β’ (π = π½ β (π₯ β βͺ π β¦ {π¦ β π β£ π₯ β π¦}) = (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦})) |
6 | 2, 5 | oveq12d 7379 |
. . . 4
β’ (π = π½ β (π qTop (π₯ β βͺ π β¦ {π¦ β π β£ π₯ β π¦})) = (π½ qTop (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦}))) |
7 | | df-kq 23068 |
. . . 4
β’ KQ =
(π β Top β¦
(π qTop (π₯ β βͺ π β¦ {π¦ β π β£ π₯ β π¦}))) |
8 | | ovex 7394 |
. . . 4
β’ (π½ qTop (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦})) β V |
9 | 6, 7, 8 | fvmpt 6952 |
. . 3
β’ (π½ β Top β
(KQβπ½) = (π½ qTop (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦}))) |
10 | 1, 9 | syl 17 |
. 2
β’ (π½ β (TopOnβπ) β (KQβπ½) = (π½ qTop (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦}))) |
11 | | kqval.2 |
. . . 4
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
12 | | toponuni 22286 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
13 | 12 | mpteq1d 5204 |
. . . 4
β’ (π½ β (TopOnβπ) β (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) = (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦})) |
14 | 11, 13 | eqtrid 2785 |
. . 3
β’ (π½ β (TopOnβπ) β πΉ = (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦})) |
15 | 14 | oveq2d 7377 |
. 2
β’ (π½ β (TopOnβπ) β (π½ qTop πΉ) = (π½ qTop (π₯ β βͺ π½ β¦ {π¦ β π½ β£ π₯ β π¦}))) |
16 | 10, 15 | eqtr4d 2776 |
1
β’ (π½ β (TopOnβπ) β (KQβπ½) = (π½ qTop πΉ)) |