Step | Hyp | Ref
| Expression |
1 | | ismri.1 |
. . . . 5
β’ π = (mrClsβπ΄) |
2 | | ismri.2 |
. . . . 5
β’ πΌ = (mrIndβπ΄) |
3 | 1, 2 | mrisval 17578 |
. . . 4
β’ (π΄ β (Mooreβπ) β πΌ = {π β π« π β£ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))}) |
4 | 3 | eleq2d 2817 |
. . 3
β’ (π΄ β (Mooreβπ) β (π β πΌ β π β {π β π« π β£ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))})) |
5 | | difeq1 4114 |
. . . . . . . 8
β’ (π = π β (π β {π₯}) = (π β {π₯})) |
6 | 5 | fveq2d 6894 |
. . . . . . 7
β’ (π = π β (πβ(π β {π₯})) = (πβ(π β {π₯}))) |
7 | 6 | eleq2d 2817 |
. . . . . 6
β’ (π = π β (π₯ β (πβ(π β {π₯})) β π₯ β (πβ(π β {π₯})))) |
8 | 7 | notbid 317 |
. . . . 5
β’ (π = π β (Β¬ π₯ β (πβ(π β {π₯})) β Β¬ π₯ β (πβ(π β {π₯})))) |
9 | 8 | raleqbi1dv 3331 |
. . . 4
β’ (π = π β (βπ₯ β π Β¬ π₯ β (πβ(π β {π₯})) β βπ₯ β π Β¬ π₯ β (πβ(π β {π₯})))) |
10 | 9 | elrab 3682 |
. . 3
β’ (π β {π β π« π β£ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))} β (π β π« π β§ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯})))) |
11 | 4, 10 | bitrdi 286 |
. 2
β’ (π΄ β (Mooreβπ) β (π β πΌ β (π β π« π β§ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))))) |
12 | | elfvex 6928 |
. . . 4
β’ (π΄ β (Mooreβπ) β π β V) |
13 | | elpw2g 5343 |
. . . 4
β’ (π β V β (π β π« π β π β π)) |
14 | 12, 13 | syl 17 |
. . 3
β’ (π΄ β (Mooreβπ) β (π β π« π β π β π)) |
15 | 14 | anbi1d 628 |
. 2
β’ (π΄ β (Mooreβπ) β ((π β π« π β§ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))) β (π β π β§ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))))) |
16 | 11, 15 | bitrd 278 |
1
β’ (π΄ β (Mooreβπ) β (π β πΌ β (π β π β§ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))))) |