| Step | Hyp | Ref
| Expression |
|---|
| 1 | | neifval.1 |
. . . 4
β’ π = βͺ
π½ |
| 2 | 1 | topopn 13593 |
. . 3
β’ (π½ β Top β π β π½) |
| 3 | | pwexg 4182 |
. . 3
β’ (π β π½ β π« π β V) |
| 4 | | mptexg 5743 |
. . 3
β’
(π« π β
V β (π₯ β
π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)}) β V) |
| 5 | 2, 3, 4 | 3syl 17 |
. 2
β’ (π½ β Top β (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)}) β V) |
| 6 | | unieq 3820 |
. . . . . 6
β’ (π = π½ β βͺ π = βͺ
π½) |
| 7 | 6, 1 | eqtr4di 2228 |
. . . . 5
β’ (π = π½ β βͺ π = π) |
| 8 | 7 | pweqd 3582 |
. . . 4
β’ (π = π½ β π« βͺ π =
π« π) |
| 9 | | rexeq 2674 |
. . . . 5
β’ (π = π½ β (βπ β π (π₯ β π β§ π β π£) β βπ β π½ (π₯ β π β§ π β π£))) |
| 10 | 8, 9 | rabeqbidv 2734 |
. . . 4
β’ (π = π½ β {π£ β π« βͺ π
β£ βπ β
π (π₯ β π β§ π β π£)} = {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)}) |
| 11 | 8, 10 | mpteq12dv 4087 |
. . 3
β’ (π = π½ β (π₯ β π« βͺ π
β¦ {π£ β π«
βͺ π β£ βπ β π (π₯ β π β§ π β π£)}) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})) |
| 12 | | df-nei 13724 |
. . 3
β’ nei =
(π β Top β¦
(π₯ β π« βͺ π
β¦ {π£ β π«
βͺ π β£ βπ β π (π₯ β π β§ π β π£)})) |
| 13 | 11, 12 | fvmptg 5594 |
. 2
β’ ((π½ β Top β§ (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)}) β V) β (neiβπ½) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})) |
| 14 | 5, 13 | mpdan 421 |
1
β’ (π½ β Top β
(neiβπ½) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})) |
