| Step | Hyp | Ref
| Expression |
|---|
| 1 | | neifval.1 |
. . . 4
β’ π = βͺ
π½ |
| 2 | 1 | neival 13728 |
. . 3
β’ ((π½ β Top β§ π β π) β ((neiβπ½)βπ) = {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)}) |
| 3 | 2 | eleq2d 2247 |
. 2
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)βπ) β π β {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)})) |
| 4 | | sseq2 3181 |
. . . . . . 7
β’ (π£ = π β (π β π£ β π β π)) |
| 5 | 4 | anbi2d 464 |
. . . . . 6
β’ (π£ = π β ((π β π β§ π β π£) β (π β π β§ π β π))) |
| 6 | 5 | rexbidv 2478 |
. . . . 5
β’ (π£ = π β (βπ β π½ (π β π β§ π β π£) β βπ β π½ (π β π β§ π β π))) |
| 7 | 6 | elrab 2895 |
. . . 4
β’ (π β {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)} β (π β π« π β§ βπ β π½ (π β π β§ π β π))) |
| 8 | 1 | topopn 13593 |
. . . . . 6
β’ (π½ β Top β π β π½) |
| 9 | | elpw2g 4158 |
. . . . . 6
β’ (π β π½ β (π β π« π β π β π)) |
| 10 | 8, 9 | syl 14 |
. . . . 5
β’ (π½ β Top β (π β π« π β π β π)) |
| 11 | 10 | anbi1d 465 |
. . . 4
β’ (π½ β Top β ((π β π« π β§ βπ β π½ (π β π β§ π β π)) β (π β π β§ βπ β π½ (π β π β§ π β π)))) |
| 12 | 7, 11 | bitrid 192 |
. . 3
β’ (π½ β Top β (π β {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)} β (π β π β§ βπ β π½ (π β π β§ π β π)))) |
| 13 | 12 | adantr 276 |
. 2
β’ ((π½ β Top β§ π β π) β (π β {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)} β (π β π β§ βπ β π½ (π β π β§ π β π)))) |
| 14 | 3, 13 | bitrd 188 |
1
β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)βπ) β (π β π β§ βπ β π½ (π β π β§ π β π)))) |
