Step | Hyp | Ref
| Expression |
1 | | df-mrc 17402 |
. . 3
β’ mrCls =
(π β βͺ ran Moore β¦ (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π })) |
2 | 1 | fnmpt 6637 |
. 2
β’
(βπ β
βͺ ran Moore(π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V β mrCls Fn βͺ ran Moore) |
3 | | mreunirn 17416 |
. . 3
β’ (π β βͺ ran Moore β π β (Mooreββͺ π)) |
4 | | mrcflem 17421 |
. . . . 5
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ) |
5 | | fssxp 6692 |
. . . . 5
β’ ((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }):π« βͺ
πβΆπ β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π)) |
7 | | vuniex 7667 |
. . . . . 6
β’ βͺ π
β V |
8 | 7 | pwex 5334 |
. . . . 5
β’ π«
βͺ π β V |
9 | | vex 3448 |
. . . . 5
β’ π β V |
10 | 8, 9 | xpex 7678 |
. . . 4
β’
(π« βͺ π Γ π) β V |
11 | | ssexg 5279 |
. . . 4
β’ (((π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β (π« βͺ π
Γ π) β§ (π«
βͺ π Γ π) β V) β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
12 | 6, 10, 11 | sylancl 587 |
. . 3
β’ (π β (Mooreββͺ π)
β (π₯ β π«
βͺ π β¦ β© {π β π β£ π₯ β π }) β V) |
13 | 3, 12 | sylbi 216 |
. 2
β’ (π β βͺ ran Moore β (π₯ β π« βͺ π
β¦ β© {π β π β£ π₯ β π }) β V) |
14 | 2, 13 | mprg 3069 |
1
β’ mrCls Fn
βͺ ran Moore |