Step | Hyp | Ref
| Expression |
1 | | psubspset.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
2 | | psubspset.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
3 | | psubspset.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
4 | | psubspset.s |
. . . . . 6
β’ π = (PSubSpβπΎ) |
5 | 1, 2, 3, 4 | ispsubsp2 38238 |
. . . . 5
β’ (πΎ β π· β (π β π β (π β π΄ β§ βπ β π΄ (βπ β π βπ β π π β€ (π β¨ π) β π β π)))) |
6 | 5 | simplbda 501 |
. . . 4
β’ ((πΎ β π· β§ π β π) β βπ β π΄ (βπ β π βπ β π π β€ (π β¨ π) β π β π)) |
7 | 6 | ex 414 |
. . 3
β’ (πΎ β π· β (π β π β βπ β π΄ (βπ β π βπ β π π β€ (π β¨ π) β π β π))) |
8 | | breq1 5113 |
. . . . . 6
β’ (π = π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
9 | 8 | 2rexbidv 3214 |
. . . . 5
β’ (π = π β (βπ β π βπ β π π β€ (π β¨ π) β βπ β π βπ β π π β€ (π β¨ π))) |
10 | | eleq1 2826 |
. . . . 5
β’ (π = π β (π β π β π β π)) |
11 | 9, 10 | imbi12d 345 |
. . . 4
β’ (π = π β ((βπ β π βπ β π π β€ (π β¨ π) β π β π) β (βπ β π βπ β π π β€ (π β¨ π) β π β π))) |
12 | 11 | rspccv 3581 |
. . 3
β’
(βπ β
π΄ (βπ β π βπ β π π β€ (π β¨ π) β π β π) β (π β π΄ β (βπ β π βπ β π π β€ (π β¨ π) β π β π))) |
13 | 7, 12 | syl6 35 |
. 2
β’ (πΎ β π· β (π β π β (π β π΄ β (βπ β π βπ β π π β€ (π β¨ π) β π β π)))) |
14 | 13 | 3imp1 1348 |
1
β’ (((πΎ β π· β§ π β π β§ π β π΄) β§ βπ β π βπ β π π β€ (π β¨ π)) β π β π) |