| Step | Hyp | Ref
| Expression |
|---|
| 1 | | df-mrc 17535 |
. . 3
β’ mrCls =
(π β βͺ ran Moore β¦ (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π })) |
| 2 | 1 | fnmpt 6689 |
. 2
β’
(βπ β
βͺ ran Moore(π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V β mrCls Fn βͺ ran Moore) |
| 3 | | mreunirn 17549 |
. . 3
β’ (π β βͺ ran Moore β π β (Mooreββͺ π)) |
| 4 | | mrcflem 17554 |
. . . . 5
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ) |
| 5 | | fssxp 6744 |
. . . . 5
β’ ((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
| 6 | 4, 5 | syl 17 |
. . . 4
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
| 7 | | vuniex 7731 |
. . . . . 6
β’ βͺ π
β V |
| 8 | 7 | pwex 5377 |
. . . . 5
β’ π«
βͺ π β V |
| 9 | | vex 3476 |
. . . . 5
β’ π β V |
| 10 | 8, 9 | xpex 7742 |
. . . 4
β’
(π« βͺ π Γ π) β V |
| 11 | | ssexg 5322 |
. . . 4
β’ (((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π) β§ (π«
βͺ π Γ π) β V) β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
| 12 | 6, 10, 11 | sylancl 584 |
. . 3
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }) β V) |
| 13 | 3, 12 | sylbi 216 |
. 2
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
| 14 | 2, 13 | mprg 3065 |
1
β’ mrCls Fn
βͺ ran Moore |
