Step | Hyp | Ref
| Expression |
1 | | mrcfval.f |
. 2
β’ πΉ = (mrClsβπΆ) |
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 | | rabeq 3447 |
. . . . . . 7
β’ (π = πΆ β {π β π β£ π₯ β π } = {π β πΆ β£ π₯ β π }) |
7 | 6 | inteqd 4956 |
. . . . . 6
β’ (π = πΆ β β© {π β π β£ π₯ β π } = β© {π β πΆ β£ π₯ β π }) |
8 | 5, 7 | mpteq12dv 5240 |
. . . . 5
β’ (π = πΆ β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) = (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π })) |
9 | | df-mrc 17531 |
. . . . 5
β’ mrCls =
(π β βͺ ran Moore β¦ (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π })) |
10 | | mreunirn 17545 |
. . . . . . . 8
β’ (π β βͺ ran Moore β π β (Mooreββͺ π)) |
11 | | mrcflem 17550 |
. . . . . . . 8
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ) |
12 | 10, 11 | sylbi 216 |
. . . . . . 7
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ) |
13 | | fssxp 6746 |
. . . . . . 7
β’ ((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
15 | | vuniex 7729 |
. . . . . . . 8
β’ βͺ π
β V |
16 | 15 | pwex 5379 |
. . . . . . 7
β’ π«
βͺ π β V |
17 | | vex 3479 |
. . . . . . 7
β’ π β V |
18 | 16, 17 | xpex 7740 |
. . . . . 6
β’
(π« βͺ π Γ π) β V |
19 | | ssexg 5324 |
. . . . . 6
β’ (((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π) β§ (π«
βͺ π Γ π) β V) β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
20 | 14, 18, 19 | sylancl 587 |
. . . . 5
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
21 | 8, 9, 20 | fvmpt3 7003 |
. . . 4
β’ (πΆ β βͺ ran Moore β (mrClsβπΆ) = (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π })) |
22 | 3, 21 | syl 17 |
. . 3
β’ (πΆ β (Mooreβπ) β (mrClsβπΆ) = (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π })) |
23 | | mreuni 17544 |
. . . . 5
β’ (πΆ β (Mooreβπ) β βͺ πΆ =
π) |
24 | 23 | pweqd 4620 |
. . . 4
β’ (πΆ β (Mooreβπ) β π« βͺ πΆ =
π« π) |
25 | 24 | mpteq1d 5244 |
. . 3
β’ (πΆ β (Mooreβπ) β (π₯ β π« βͺ πΆ
β¦ β© {π β πΆ β£ π₯ β π }) = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
26 | 22, 25 | eqtrd 2773 |
. 2
β’ (πΆ β (Mooreβπ) β (mrClsβπΆ) = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
27 | 1, 26 | eqtrid 2785 |
1
β’ (πΆ β (Mooreβπ) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |