Step | Hyp | Ref
| Expression |
1 | | simp33 1212 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β (π β¨ π) β€ (π
β¨ π)) |
2 | | simp1 1137 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β πΎ β HL) |
3 | | simp21 1207 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β π β π΄) |
4 | | simp22 1208 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β π β π΄) |
5 | | simp23 1209 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β π β π) |
6 | | simp31 1210 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β π
β π΄) |
7 | | simp32 1211 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β π β π΄) |
8 | | ps1.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
9 | | ps1.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
10 | | ps1.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
11 | 8, 9, 10 | ps-1 37969 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄)) β ((π β¨ π) β€ (π
β¨ π) β (π β¨ π) = (π
β¨ π))) |
12 | 2, 3, 4, 5, 6, 7, 11 | syl132anc 1389 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β ((π β¨ π) β€ (π
β¨ π) β (π β¨ π) = (π
β¨ π))) |
13 | 1, 12 | mpbid 231 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β (π β¨ π) = (π
β¨ π)) |
14 | 9, 10 | lnnat 37919 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ (π β¨ π) β π΄)) |
15 | 2, 3, 4, 14 | syl3anc 1372 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β (π β π β Β¬ (π β¨ π) β π΄)) |
16 | 5, 15 | mpbid 231 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β Β¬ (π β¨ π) β π΄) |
17 | 13, 16 | eqneltrrd 2859 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β Β¬ (π
β¨ π) β π΄) |
18 | 9, 10 | lnnat 37919 |
. . 3
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β π β Β¬ (π
β¨ π) β π΄)) |
19 | 2, 6, 7, 18 | syl3anc 1372 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β (π
β π β Β¬ (π
β¨ π) β π΄)) |
20 | 17, 19 | mpbird 257 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π
β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π
β¨ π))) β π
β π) |