Step | Hyp | Ref
| Expression |
1 | | mrcfval.f |
. . . 4
β’ πΉ = (mrClsβπΆ) |
2 | 1 | mrcfval 17495 |
. . 3
β’ (πΆ β (Mooreβπ) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
3 | 2 | adantr 482 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π) β πΉ = (π₯ β π« π β¦ β© {π β πΆ β£ π₯ β π })) |
4 | | sseq1 3974 |
. . . . 5
β’ (π₯ = π β (π₯ β π β π β π )) |
5 | 4 | rabbidv 3418 |
. . . 4
β’ (π₯ = π β {π β πΆ β£ π₯ β π } = {π β πΆ β£ π β π }) |
6 | 5 | inteqd 4917 |
. . 3
β’ (π₯ = π β β© {π β πΆ β£ π₯ β π } = β© {π β πΆ β£ π β π }) |
7 | 6 | adantl 483 |
. 2
β’ (((πΆ β (Mooreβπ) β§ π β π) β§ π₯ = π) β β© {π β πΆ β£ π₯ β π } = β© {π β πΆ β£ π β π }) |
8 | | mre1cl 17481 |
. . . 4
β’ (πΆ β (Mooreβπ) β π β πΆ) |
9 | | elpw2g 5306 |
. . . 4
β’ (π β πΆ β (π β π« π β π β π)) |
10 | 8, 9 | syl 17 |
. . 3
β’ (πΆ β (Mooreβπ) β (π β π« π β π β π)) |
11 | 10 | biimpar 479 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π« π) |
12 | | sseq2 3975 |
. . . . 5
β’ (π = π β (π β π β π β π)) |
13 | 8 | adantr 482 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β πΆ) |
14 | | simpr 486 |
. . . . 5
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β π) |
15 | 12, 13, 14 | elrabd 3652 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ π β π) β π β {π β πΆ β£ π β π }) |
16 | 15 | ne0d 4300 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ π β π) β {π β πΆ β£ π β π } β β
) |
17 | | intex 5299 |
. . 3
β’ ({π β πΆ β£ π β π } β β
β β© {π
β πΆ β£ π β π } β V) |
18 | 16, 17 | sylib 217 |
. 2
β’ ((πΆ β (Mooreβπ) β§ π β π) β β© {π β πΆ β£ π β π } β V) |
19 | 3, 7, 11, 18 | fvmptd 6960 |
1
β’ ((πΆ β (Mooreβπ) β§ π β π) β (πΉβπ) = β© {π β πΆ β£ π β π }) |