Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . . 6
β’ ((πΎ β π β§ π β π β§ π β π) β πΎ β π) |
2 | | simp2 1137 |
. . . . . . 7
β’ ((πΎ β π β§ π β π β§ π β π) β π β π) |
3 | | eqid 2732 |
. . . . . . . . 9
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | elpcli.s |
. . . . . . . . 9
β’ π = (PSubSpβπΎ) |
5 | 3, 4 | psubssat 38620 |
. . . . . . . 8
β’ ((πΎ β π β§ π β π) β π β (AtomsβπΎ)) |
6 | 5 | 3adant2 1131 |
. . . . . . 7
β’ ((πΎ β π β§ π β π β§ π β π) β π β (AtomsβπΎ)) |
7 | 2, 6 | sstrd 3992 |
. . . . . 6
β’ ((πΎ β π β§ π β π β§ π β π) β π β (AtomsβπΎ)) |
8 | | elpcli.c |
. . . . . . 7
β’ π = (PClβπΎ) |
9 | 3, 4, 8 | pclvalN 38756 |
. . . . . 6
β’ ((πΎ β π β§ π β (AtomsβπΎ)) β (πβπ) = β© {π§ β π β£ π β π§}) |
10 | 1, 7, 9 | syl2anc 584 |
. . . . 5
β’ ((πΎ β π β§ π β π β§ π β π) β (πβπ) = β© {π§ β π β£ π β π§}) |
11 | 10 | eleq2d 2819 |
. . . 4
β’ ((πΎ β π β§ π β π β§ π β π) β (π β (πβπ) β π β β© {π§ β π β£ π β π§})) |
12 | | elintrabg 4965 |
. . . . 5
β’ (π β β© {π§
β π β£ π β π§} β (π β β© {π§ β π β£ π β π§} β βπ§ β π (π β π§ β π β π§))) |
13 | 12 | ibi 266 |
. . . 4
β’ (π β β© {π§
β π β£ π β π§} β βπ§ β π (π β π§ β π β π§)) |
14 | 11, 13 | syl6bi 252 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π) β (π β (πβπ) β βπ§ β π (π β π§ β π β π§))) |
15 | | sseq2 4008 |
. . . . . . . 8
β’ (π§ = π β (π β π§ β π β π)) |
16 | | eleq2 2822 |
. . . . . . . 8
β’ (π§ = π β (π β π§ β π β π)) |
17 | 15, 16 | imbi12d 344 |
. . . . . . 7
β’ (π§ = π β ((π β π§ β π β π§) β (π β π β π β π))) |
18 | 17 | rspccv 3609 |
. . . . . 6
β’
(βπ§ β
π (π β π§ β π β π§) β (π β π β (π β π β π β π))) |
19 | 18 | com13 88 |
. . . . 5
β’ (π β π β (π β π β (βπ§ β π (π β π§ β π β π§) β π β π))) |
20 | 19 | imp 407 |
. . . 4
β’ ((π β π β§ π β π) β (βπ§ β π (π β π§ β π β π§) β π β π)) |
21 | 20 | 3adant1 1130 |
. . 3
β’ ((πΎ β π β§ π β π β§ π β π) β (βπ§ β π (π β π§ β π β π§) β π β π)) |
22 | 14, 21 | syld 47 |
. 2
β’ ((πΎ β π β§ π β π β§ π β π) β (π β (πβπ) β π β π)) |
23 | 22 | imp 407 |
1
β’ (((πΎ β π β§ π β π β§ π β π) β§ π β (πβπ)) β π β π) |