Step | Hyp | Ref
| Expression |
1 | | sstr2 3952 |
. . . . . 6
β’ (π β π β (π β π¦ β π β π¦)) |
2 | 1 | 3ad2ant2 1135 |
. . . . 5
β’ ((πΎ β π β§ π β π β§ π β π΄) β (π β π¦ β π β π¦)) |
3 | 2 | adantr 482 |
. . . 4
β’ (((πΎ β π β§ π β π β§ π β π΄) β§ π¦ β (PSubSpβπΎ)) β (π β π¦ β π β π¦)) |
4 | 3 | ss2rabdv 4034 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π΄) β {π¦ β (PSubSpβπΎ) β£ π β π¦} β {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
5 | | intss 4931 |
. . 3
β’ ({π¦ β (PSubSpβπΎ) β£ π β π¦} β {π¦ β (PSubSpβπΎ) β£ π β π¦} β β© {π¦ β (PSubSpβπΎ) β£ π β π¦} β β© {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
6 | 4, 5 | syl 17 |
. 2
β’ ((πΎ β π β§ π β π β§ π β π΄) β β© {π¦ β (PSubSpβπΎ) β£ π β π¦} β β© {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
7 | | simp1 1137 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π΄) β πΎ β π) |
8 | | sstr 3953 |
. . . 4
β’ ((π β π β§ π β π΄) β π β π΄) |
9 | 8 | 3adant1 1131 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π΄) β π β π΄) |
10 | | pclss.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
11 | | eqid 2737 |
. . . 4
β’
(PSubSpβπΎ) =
(PSubSpβπΎ) |
12 | | pclss.c |
. . . 4
β’ π = (PClβπΎ) |
13 | 10, 11, 12 | pclvalN 38356 |
. . 3
β’ ((πΎ β π β§ π β π΄) β (πβπ) = β© {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
14 | 7, 9, 13 | syl2anc 585 |
. 2
β’ ((πΎ β π β§ π β π β§ π β π΄) β (πβπ) = β© {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
15 | 10, 11, 12 | pclvalN 38356 |
. . 3
β’ ((πΎ β π β§ π β π΄) β (πβπ) = β© {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
16 | 15 | 3adant2 1132 |
. 2
β’ ((πΎ β π β§ π β π β§ π β π΄) β (πβπ) = β© {π¦ β (PSubSpβπΎ) β£ π β π¦}) |
17 | 6, 14, 16 | 3sstr4d 3992 |
1
β’ ((πΎ β π β§ π β π β§ π β π΄) β (πβπ) β (πβπ)) |