Step | Hyp | Ref
| Expression |
1 | | pclfval.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
2 | 1 | fvexi 6857 |
. . 3
β’ π΄ β V |
3 | 2 | elpw2 5303 |
. 2
β’ (π β π« π΄ β π β π΄) |
4 | | pclfval.s |
. . . . . 6
β’ π = (PSubSpβπΎ) |
5 | | pclfval.c |
. . . . . 6
β’ π = (PClβπΎ) |
6 | 1, 4, 5 | pclfvalN 38355 |
. . . . 5
β’ (πΎ β π β π = (π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦})) |
7 | 6 | fveq1d 6845 |
. . . 4
β’ (πΎ β π β (πβπ) = ((π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦})βπ)) |
8 | 7 | adantr 482 |
. . 3
β’ ((πΎ β π β§ π β π« π΄) β (πβπ) = ((π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦})βπ)) |
9 | | eqid 2737 |
. . . 4
β’ (π₯ β π« π΄ β¦ β© {π¦
β π β£ π₯ β π¦}) = (π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦}) |
10 | | sseq1 3970 |
. . . . . 6
β’ (π₯ = π β (π₯ β π¦ β π β π¦)) |
11 | 10 | rabbidv 3416 |
. . . . 5
β’ (π₯ = π β {π¦ β π β£ π₯ β π¦} = {π¦ β π β£ π β π¦}) |
12 | 11 | inteqd 4913 |
. . . 4
β’ (π₯ = π β β© {π¦ β π β£ π₯ β π¦} = β© {π¦ β π β£ π β π¦}) |
13 | | simpr 486 |
. . . 4
β’ ((πΎ β π β§ π β π« π΄) β π β π« π΄) |
14 | | elpwi 4568 |
. . . . . . . 8
β’ (π β π« π΄ β π β π΄) |
15 | 14 | adantl 483 |
. . . . . . 7
β’ ((πΎ β π β§ π β π« π΄) β π β π΄) |
16 | 1, 4 | atpsubN 38219 |
. . . . . . . . 9
β’ (πΎ β π β π΄ β π) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β π β§ π β π« π΄) β π΄ β π) |
18 | | sseq2 3971 |
. . . . . . . . 9
β’ (π¦ = π΄ β (π β π¦ β π β π΄)) |
19 | 18 | elrab3 3647 |
. . . . . . . 8
β’ (π΄ β π β (π΄ β {π¦ β π β£ π β π¦} β π β π΄)) |
20 | 17, 19 | syl 17 |
. . . . . . 7
β’ ((πΎ β π β§ π β π« π΄) β (π΄ β {π¦ β π β£ π β π¦} β π β π΄)) |
21 | 15, 20 | mpbird 257 |
. . . . . 6
β’ ((πΎ β π β§ π β π« π΄) β π΄ β {π¦ β π β£ π β π¦}) |
22 | 21 | ne0d 4296 |
. . . . 5
β’ ((πΎ β π β§ π β π« π΄) β {π¦ β π β£ π β π¦} β β
) |
23 | | intex 5295 |
. . . . 5
β’ ({π¦ β π β£ π β π¦} β β
β β© {π¦
β π β£ π β π¦} β V) |
24 | 22, 23 | sylib 217 |
. . . 4
β’ ((πΎ β π β§ π β π« π΄) β β© {π¦ β π β£ π β π¦} β V) |
25 | 9, 12, 13, 24 | fvmptd3 6972 |
. . 3
β’ ((πΎ β π β§ π β π« π΄) β ((π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦})βπ) = β© {π¦ β π β£ π β π¦}) |
26 | 8, 25 | eqtrd 2777 |
. 2
β’ ((πΎ β π β§ π β π« π΄) β (πβπ) = β© {π¦ β π β£ π β π¦}) |
27 | 3, 26 | sylan2br 596 |
1
β’ ((πΎ β π β§ π β π΄) β (πβπ) = β© {π¦ β π β£ π β π¦}) |