Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . . 6
β’ ((πΎ β π β§ π β π β§ π β π) β πΎ β π) |
2 | | simp2 1138 |
. . . . . . 7
β’ ((πΎ β π β§ π β π β§ π β π) β π β π) |
3 | | eqid 2737 |
. . . . . . . . 9
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | elpcli.s |
. . . . . . . . 9
β’ π = (PSubSpβπΎ) |
5 | 3, 4 | psubssat 38220 |
. . . . . . . 8
β’ ((πΎ β π β§ π β π) β π β (AtomsβπΎ)) |
6 | 5 | 3adant2 1132 |
. . . . . . 7
β’ ((πΎ β π β§ π β π β§ π β π) β π β (AtomsβπΎ)) |
7 | 2, 6 | sstrd 3955 |
. . . . . 6
β’ ((πΎ β π β§ π β π β§ π β π) β π β (AtomsβπΎ)) |
8 | | elpcli.c |
. . . . . . 7
β’ π = (PClβπΎ) |
9 | 3, 4, 8 | pclvalN 38356 |
. . . . . 6
β’ ((πΎ β π β§ π β (AtomsβπΎ)) β (πβπ) = β© {π§ β π β£ π β π§}) |
10 | 1, 7, 9 | syl2anc 585 |
. . . . 5
β’ ((πΎ β π β§ π β π β§ π β π) β (πβπ) = β© {π§ β π β£ π β π§}) |
11 | 10 | eleq2d 2824 |
. . . 4
β’ ((πΎ β π β§ π β π β§ π β π) β (π β (πβπ) β π β β© {π§ β π β£ π β π§})) |
12 | | elintrabg 4923 |
. . . . 5
β’ (π β β© {π§
β π β£ π β π§} β (π β β© {π§ β π β£ π β π§} β βπ§ β π (π β π§ β π β π§))) |
13 | 12 | ibi 267 |
. . . 4
β’ (π β β© {π§
β π β£ π β π§} β βπ§ β π (π β π§ β π β π§)) |
14 | 11, 13 | syl6bi 253 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π) β (π β (πβπ) β βπ§ β π (π β π§ β π β π§))) |
15 | | sseq2 3971 |
. . . . . . . 8
β’ (π§ = π β (π β π§ β π β π)) |
16 | | eleq2 2827 |
. . . . . . . 8
β’ (π§ = π β (π β π§ β π β π)) |
17 | 15, 16 | imbi12d 345 |
. . . . . . 7
β’ (π§ = π β ((π β π§ β π β π§) β (π β π β π β π))) |
18 | 17 | rspccv 3579 |
. . . . . 6
β’
(βπ§ β
π (π β π§ β π β π§) β (π β π β (π β π β π β π))) |
19 | 18 | com13 88 |
. . . . 5
β’ (π β π β (π β π β (βπ§ β π (π β π§ β π β π§) β π β π))) |
20 | 19 | imp 408 |
. . . 4
β’ ((π β π β§ π β π) β (βπ§ β π (π β π§ β π β π§) β π β π)) |
21 | 20 | 3adant1 1131 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π) β (βπ§ β π (π β π§ β π β π§) β π β π)) |
22 | 14, 21 | syld 47 |
. 2
β’ ((πΎ β π β§ π β π β§ π β π) β (π β (πβπ) β π β π)) |
23 | 22 | imp 408 |
1
β’ (((πΎ β π β§ π β π β§ π β π) β§ π β (πβπ)) β π β π) |