Step | Hyp | Ref
| Expression |
1 | | mrisval.2 |
. . 3
β’ πΌ = (mrIndβπ΄) |
2 | | fvssunirn 6925 |
. . . . 5
β’
(Mooreβπ)
β βͺ ran Moore |
3 | 2 | sseli 3979 |
. . . 4
β’ (π΄ β (Mooreβπ) β π΄ β βͺ ran
Moore) |
4 | | unieq 4920 |
. . . . . . 7
β’ (π = π΄ β βͺ π = βͺ
π΄) |
5 | 4 | pweqd 4620 |
. . . . . 6
β’ (π = π΄ β π« βͺ π =
π« βͺ π΄) |
6 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = π΄ β (mrClsβπ) = (mrClsβπ΄)) |
7 | | mrisval.1 |
. . . . . . . . . . 11
β’ π = (mrClsβπ΄) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (π = π΄ β (mrClsβπ) = π) |
9 | 8 | fveq1d 6894 |
. . . . . . . . 9
β’ (π = π΄ β ((mrClsβπ)β(π β {π₯})) = (πβ(π β {π₯}))) |
10 | 9 | eleq2d 2820 |
. . . . . . . 8
β’ (π = π΄ β (π₯ β ((mrClsβπ)β(π β {π₯})) β π₯ β (πβ(π β {π₯})))) |
11 | 10 | notbid 318 |
. . . . . . 7
β’ (π = π΄ β (Β¬ π₯ β ((mrClsβπ)β(π β {π₯})) β Β¬ π₯ β (πβ(π β {π₯})))) |
12 | 11 | ralbidv 3178 |
. . . . . 6
β’ (π = π΄ β (βπ₯ β π Β¬ π₯ β ((mrClsβπ)β(π β {π₯})) β βπ₯ β π Β¬ π₯ β (πβ(π β {π₯})))) |
13 | 5, 12 | rabeqbidv 3450 |
. . . . 5
β’ (π = π΄ β {π β π« βͺ π
β£ βπ₯ β
π Β¬ π₯ β ((mrClsβπ)β(π β {π₯}))} = {π β π« βͺ π΄
β£ βπ₯ β
π Β¬ π₯ β (πβ(π β {π₯}))}) |
14 | | df-mri 17532 |
. . . . 5
β’ mrInd =
(π β βͺ ran Moore β¦ {π β π« βͺ π
β£ βπ₯ β
π Β¬ π₯ β ((mrClsβπ)β(π β {π₯}))}) |
15 | | vuniex 7729 |
. . . . . . 7
β’ βͺ π
β V |
16 | 15 | pwex 5379 |
. . . . . 6
β’ π«
βͺ π β V |
17 | 16 | rabex 5333 |
. . . . 5
β’ {π β π« βͺ π
β£ βπ₯ β
π Β¬ π₯ β ((mrClsβπ)β(π β {π₯}))} β V |
18 | 13, 14, 17 | fvmpt3i 7004 |
. . . 4
β’ (π΄ β βͺ ran Moore β (mrIndβπ΄) = {π β π« βͺ π΄
β£ βπ₯ β
π Β¬ π₯ β (πβ(π β {π₯}))}) |
19 | 3, 18 | syl 17 |
. . 3
β’ (π΄ β (Mooreβπ) β (mrIndβπ΄) = {π β π« βͺ π΄
β£ βπ₯ β
π Β¬ π₯ β (πβ(π β {π₯}))}) |
20 | 1, 19 | eqtrid 2785 |
. 2
β’ (π΄ β (Mooreβπ) β πΌ = {π β π« βͺ π΄
β£ βπ₯ β
π Β¬ π₯ β (πβ(π β {π₯}))}) |
21 | | mreuni 17544 |
. . . 4
β’ (π΄ β (Mooreβπ) β βͺ π΄ =
π) |
22 | 21 | pweqd 4620 |
. . 3
β’ (π΄ β (Mooreβπ) β π« βͺ π΄ =
π« π) |
23 | 22 | rabeqdv 3448 |
. 2
β’ (π΄ β (Mooreβπ) β {π β π« βͺ π΄
β£ βπ₯ β
π Β¬ π₯ β (πβ(π β {π₯}))} = {π β π« π β£ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))}) |
24 | 20, 23 | eqtrd 2773 |
1
β’ (π΄ β (Mooreβπ) β πΌ = {π β π« π β£ βπ₯ β π Β¬ π₯ β (πβ(π β {π₯}))}) |