Step | Hyp | Ref
| Expression |
1 | | mrcfval.f |
. . . 4
β’ πΉ = (mrClsβπΆ) |
2 | 1 | mrcfval 17548 |
. . 3
β’ (πΆ β (Mooreβπ) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
3 | 2 | adantr 481 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
4 | | sseq1 4006 |
. . . . 5
β’ (π₯ = π β (π₯ β π β π β π )) |
5 | 4 | rabbidv 3440 |
. . . 4
β’ (π₯ = π β {π β πΆ β£ π₯ β π } = {π β πΆ β£ π β π }) |
6 | 5 | inteqd 4954 |
. . 3
β’ (π₯ = π β β© {π β πΆ β£ π₯ β π } = β© {π β πΆ β£ π β π }) |
7 | 6 | adantl 482 |
. 2
β’ (((πΆ β (Mooreβπ) β§ π β π) β§ π₯ = π) β β© {π β πΆ β£ π₯ β π } = β© {π β πΆ β£ π β π }) |
8 | | mre1cl 17534 |
. . . 4
β’ (πΆ β (Mooreβπ) β π β πΆ) |
9 | | elpw2g 5343 |
. . . 4
β’ (π β πΆ β (π β π« π β π β π)) |
10 | 8, 9 | syl 17 |
. . 3
β’ (πΆ β (Mooreβπ) β (π β π« π β π β π)) |
11 | 10 | biimpar 478 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π« π) |
12 | | sseq2 4007 |
. . . . 5
β’ (π = π β (π β π β π β π)) |
13 | 8 | adantr 481 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β πΆ) |
14 | | simpr 485 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π) |
15 | 12, 13, 14 | elrabd 3684 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β {π β πΆ β£ π β π }) |
16 | 15 | ne0d 4334 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π) β {π β πΆ β£ π β π } β β
) |
17 | | intex 5336 |
. . 3
β’ ({π β πΆ β£ π β π } β β
β β© {π
β πΆ β£ π β π } β V) |
18 | 16, 17 | sylib 217 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π) β β© {π β πΆ β£ π β π } β V) |
19 | 3, 7, 11, 18 | fvmptd 7002 |
1
β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβπ) = β© {π β πΆ β£ π β π }) |