Step | Hyp | Ref
| Expression |
1 | | pclfval.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
2 | | pclfval.s |
. . 3
β’ π = (PSubSpβπΎ) |
3 | | pclfval.c |
. . 3
β’ π = (PClβπΎ) |
4 | 1, 2, 3 | pclvalN 38356 |
. 2
β’ ((πΎ β π β§ π β π΄) β (πβπ) = β© {π¦ β π β£ π β π¦}) |
5 | 1, 2 | atpsubN 38219 |
. . . 4
β’ (πΎ β π β π΄ β π) |
6 | | sseq2 3971 |
. . . . 5
β’ (π¦ = π΄ β (π β π¦ β π β π΄)) |
7 | 6 | intminss 4936 |
. . . 4
β’ ((π΄ β π β§ π β π΄) β β© {π¦ β π β£ π β π¦} β π΄) |
8 | 5, 7 | sylan 581 |
. . 3
β’ ((πΎ β π β§ π β π΄) β β© {π¦ β π β£ π β π¦} β π΄) |
9 | | r19.26 3115 |
. . . . . . . 8
β’
(βπ¦ β
π ((π β π¦ β π β π¦) β§ (π β π¦ β π β π¦)) β (βπ¦ β π (π β π¦ β π β π¦) β§ βπ¦ β π (π β π¦ β π β π¦))) |
10 | | jcab 519 |
. . . . . . . . 9
β’ ((π β π¦ β (π β π¦ β§ π β π¦)) β ((π β π¦ β π β π¦) β§ (π β π¦ β π β π¦))) |
11 | 10 | ralbii 3097 |
. . . . . . . 8
β’
(βπ¦ β
π (π β π¦ β (π β π¦ β§ π β π¦)) β βπ¦ β π ((π β π¦ β π β π¦) β§ (π β π¦ β π β π¦))) |
12 | | vex 3450 |
. . . . . . . . . 10
β’ π β V |
13 | 12 | elintrab 4922 |
. . . . . . . . 9
β’ (π β β© {π¦
β π β£ π β π¦} β βπ¦ β π (π β π¦ β π β π¦)) |
14 | | vex 3450 |
. . . . . . . . . 10
β’ π β V |
15 | 14 | elintrab 4922 |
. . . . . . . . 9
β’ (π β β© {π¦
β π β£ π β π¦} β βπ¦ β π (π β π¦ β π β π¦)) |
16 | 13, 15 | anbi12i 628 |
. . . . . . . 8
β’ ((π β β© {π¦
β π β£ π β π¦} β§ π β β© {π¦ β π β£ π β π¦}) β (βπ¦ β π (π β π¦ β π β π¦) β§ βπ¦ β π (π β π¦ β π β π¦))) |
17 | 9, 11, 16 | 3bitr4ri 304 |
. . . . . . 7
β’ ((π β β© {π¦
β π β£ π β π¦} β§ π β β© {π¦ β π β£ π β π¦}) β βπ¦ β π (π β π¦ β (π β π¦ β§ π β π¦))) |
18 | | simpll1 1213 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β πΎ β π) |
19 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β π¦ β π) |
20 | | simpll3 1215 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β π β π΄) |
21 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β π β π¦) |
22 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β π β π¦) |
23 | | simpll2 1214 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β π(leβπΎ)(π(joinβπΎ)π)) |
24 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(leβπΎ) =
(leβπΎ) |
25 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’
(joinβπΎ) =
(joinβπΎ) |
26 | 24, 25, 1, 2 | psubspi2N 38214 |
. . . . . . . . . . . . . 14
β’ (((πΎ β π β§ π¦ β π β§ π β π΄) β§ (π β π¦ β§ π β π¦ β§ π(leβπΎ)(π(joinβπΎ)π))) β π β π¦) |
27 | 18, 19, 20, 21, 22, 23, 26 | syl33anc 1386 |
. . . . . . . . . . . . 13
β’ ((((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β§ (π β π¦ β§ π β π¦)) β π β π¦) |
28 | 27 | ex 414 |
. . . . . . . . . . . 12
β’ (((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β ((π β π¦ β§ π β π¦) β π β π¦)) |
29 | 28 | imim2d 57 |
. . . . . . . . . . 11
β’ (((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β§ π¦ β π) β ((π β π¦ β (π β π¦ β§ π β π¦)) β (π β π¦ β π β π¦))) |
30 | 29 | ralimdva 3165 |
. . . . . . . . . 10
β’ ((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β (βπ¦ β π (π β π¦ β (π β π¦ β§ π β π¦)) β βπ¦ β π (π β π¦ β π β π¦))) |
31 | | vex 3450 |
. . . . . . . . . . 11
β’ π β V |
32 | 31 | elintrab 4922 |
. . . . . . . . . 10
β’ (π β β© {π¦
β π β£ π β π¦} β βπ¦ β π (π β π¦ β π β π¦)) |
33 | 30, 32 | syl6ibr 252 |
. . . . . . . . 9
β’ ((πΎ β π β§ π(leβπΎ)(π(joinβπΎ)π) β§ π β π΄) β (βπ¦ β π (π β π¦ β (π β π¦ β§ π β π¦)) β π β β© {π¦ β π β£ π β π¦})) |
34 | 33 | 3exp 1120 |
. . . . . . . 8
β’ (πΎ β π β (π(leβπΎ)(π(joinβπΎ)π) β (π β π΄ β (βπ¦ β π (π β π¦ β (π β π¦ β§ π β π¦)) β π β β© {π¦ β π β£ π β π¦})))) |
35 | 34 | com24 95 |
. . . . . . 7
β’ (πΎ β π β (βπ¦ β π (π β π¦ β (π β π¦ β§ π β π¦)) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦})))) |
36 | 17, 35 | biimtrid 241 |
. . . . . 6
β’ (πΎ β π β ((π β β© {π¦ β π β£ π β π¦} β§ π β β© {π¦ β π β£ π β π¦}) β (π β π΄ β (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦})))) |
37 | 36 | ralrimdv 3150 |
. . . . 5
β’ (πΎ β π β ((π β β© {π¦ β π β£ π β π¦} β§ π β β© {π¦ β π β£ π β π¦}) β βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦}))) |
38 | 37 | ralrimivv 3196 |
. . . 4
β’ (πΎ β π β βπ β β© {π¦ β π β£ π β π¦}βπ β β© {π¦ β π β£ π β π¦}βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦})) |
39 | 38 | adantr 482 |
. . 3
β’ ((πΎ β π β§ π β π΄) β βπ β β© {π¦ β π β£ π β π¦}βπ β β© {π¦ β π β£ π β π¦}βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦})) |
40 | 24, 25, 1, 2 | ispsubsp 38211 |
. . . 4
β’ (πΎ β π β (β© {π¦ β π β£ π β π¦} β π β (β© {π¦ β π β£ π β π¦} β π΄ β§ βπ β β© {π¦ β π β£ π β π¦}βπ β β© {π¦ β π β£ π β π¦}βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦})))) |
41 | 40 | adantr 482 |
. . 3
β’ ((πΎ β π β§ π β π΄) β (β©
{π¦ β π β£ π β π¦} β π β (β© {π¦ β π β£ π β π¦} β π΄ β§ βπ β β© {π¦ β π β£ π β π¦}βπ β β© {π¦ β π β£ π β π¦}βπ β π΄ (π(leβπΎ)(π(joinβπΎ)π) β π β β© {π¦ β π β£ π β π¦})))) |
42 | 8, 39, 41 | mpbir2and 712 |
. 2
β’ ((πΎ β π β§ π β π΄) β β© {π¦ β π β£ π β π¦} β π) |
43 | 4, 42 | eqeltrd 2838 |
1
β’ ((πΎ β π β§ π β π΄) β (πβπ) β π) |