Step | Hyp | Ref
| Expression |
1 | | mrcfval.f |
. 2
β’ πΉ = (mrClsβπΆ) |
2 | | fvssunirn 6871 |
. . . . 5
β’
(Mooreβπ)
β βͺ ran Moore |
3 | 2 | sseli 3939 |
. . . 4
β’ (πΆ β (Mooreβπ) β πΆ β βͺ ran
Moore) |
4 | | unieq 4875 |
. . . . . . 7
β’ (π = πΆ β βͺ π = βͺ
πΆ) |
5 | 4 | pweqd 4576 |
. . . . . 6
β’ (π = πΆ β π« βͺ π =
π« βͺ πΆ) |
6 | | rabeq 3420 |
. . . . . . 7
β’ (π = πΆ β {π β π β£ π₯ β π } = {π β πΆ β£ π₯ β π }) |
7 | 6 | inteqd 4911 |
. . . . . 6
β’ (π = πΆ β β© {π β π β£ π₯ β π } = β© {π β πΆ β£ π₯ β π }) |
8 | 5, 7 | mpteq12dv 5195 |
. . . . 5
β’ (π = πΆ β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) = (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π })) |
9 | | df-mrc 17402 |
. . . . 5
β’ mrCls =
(π β βͺ ran Moore β¦ (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π })) |
10 | | mreunirn 17416 |
. . . . . . . 8
β’ (π β βͺ ran Moore β π β (Mooreββͺ π)) |
11 | | mrcflem 17421 |
. . . . . . . 8
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ) |
12 | 10, 11 | sylbi 216 |
. . . . . . 7
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ) |
13 | | fssxp 6692 |
. . . . . . 7
β’ ((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
15 | | vuniex 7667 |
. . . . . . . 8
β’ βͺ π
β V |
16 | 15 | pwex 5334 |
. . . . . . 7
β’ π«
βͺ π β V |
17 | | vex 3448 |
. . . . . . 7
β’ π β V |
18 | 16, 17 | xpex 7678 |
. . . . . 6
β’
(π« βͺ π Γ π) β V |
19 | | ssexg 5279 |
. . . . . 6
β’ (((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π) β§ (π«
βͺ π Γ π) β V) β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
20 | 14, 18, 19 | sylancl 587 |
. . . . 5
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
21 | 8, 9, 20 | fvmpt3 6948 |
. . . 4
β’ (πΆ β βͺ ran Moore β (mrClsβπΆ) = (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π })) |
22 | 3, 21 | syl 17 |
. . 3
β’ (πΆ β (Mooreβπ) β (mrClsβπΆ) = (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π })) |
23 | | mreuni 17415 |
. . . . 5
β’ (πΆ β (Mooreβπ) β βͺ πΆ =
π) |
24 | 23 | pweqd 4576 |
. . . 4
β’ (πΆ β (Mooreβπ) β π« βͺ πΆ =
π« π) |
25 | 24 | mpteq1d 5199 |
. . 3
β’ (πΆ β (Mooreβπ) β (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π }) = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
26 | 22, 25 | eqtrd 2778 |
. 2
β’ (πΆ β (Mooreβπ) β (mrClsβπΆ) = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
27 | 1, 26 | eqtrid 2790 |
1
β’ (πΆ β (Mooreβπ) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |