| Step | Hyp | Ref
| Expression |
|---|
| 1 | | neifval.1 |
. . . . 5
β’ π = βͺ
π½ |
| 2 | 1 | neifval 23021 |
. . . 4
β’ (π½ β Top β
(neiβπ½) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})) |
| 3 | 2 | fveq1d 6902 |
. . 3
β’ (π½ β Top β
((neiβπ½)βπ) = ((π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})βπ)) |
| 4 | 3 | adantr 479 |
. 2
β’ ((π½ β Top β§ π β π) β ((neiβπ½)βπ) = ((π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})βπ)) |
| 5 | | eqid 2727 |
. . 3
β’ (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)}) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)}) |
| 6 | | cleq1lem 14967 |
. . . . 5
β’ (π₯ = π β ((π₯ β π β§ π β π£) β (π β π β§ π β π£))) |
| 7 | 6 | rexbidv 3174 |
. . . 4
β’ (π₯ = π β (βπ β π½ (π₯ β π β§ π β π£) β βπ β π½ (π β π β§ π β π£))) |
| 8 | 7 | rabbidv 3436 |
. . 3
β’ (π₯ = π β {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)} = {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)}) |
| 9 | 1 | topopn 22826 |
. . . . 5
β’ (π½ β Top β π β π½) |
| 10 | | elpw2g 5348 |
. . . . 5
β’ (π β π½ β (π β π« π β π β π)) |
| 11 | 9, 10 | syl 17 |
. . . 4
β’ (π½ β Top β (π β π« π β π β π)) |
| 12 | 11 | biimpar 476 |
. . 3
β’ ((π½ β Top β§ π β π) β π β π« π) |
| 13 | | pwexg 5380 |
. . . . 5
β’ (π β π½ β π« π β V) |
| 14 | | rabexg 5335 |
. . . . 5
β’
(π« π β
V β {π£ β
π« π β£
βπ β π½ (π β π β§ π β π£)} β V) |
| 15 | 9, 13, 14 | 3syl 18 |
. . . 4
β’ (π½ β Top β {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)} β V) |
| 16 | 15 | adantr 479 |
. . 3
β’ ((π½ β Top β§ π β π) β {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)} β V) |
| 17 | 5, 8, 12, 16 | fvmptd3 7031 |
. 2
β’ ((π½ β Top β§ π β π) β ((π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})βπ) = {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)}) |
| 18 | 4, 17 | eqtrd 2767 |
1
β’ ((π½ β Top β§ π β π) β ((neiβπ½)βπ) = {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)}) |
