Step | Hyp | Ref
| Expression |
1 | | simp11 1202 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β πΎ β HL) |
2 | | simp2 1136 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β π β π΄) |
3 | 2 | snssd 4812 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β {π} β π΄) |
4 | | simp12 1203 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β π β π΄) |
5 | | osumcllem.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
6 | | osumcllem.p |
. . . . . 6
β’ + =
(+πβπΎ) |
7 | 5, 6 | sspadd2 38991 |
. . . . 5
β’ ((πΎ β HL β§ {π} β π΄ β§ π β π΄) β {π} β (π + {π})) |
8 | 1, 3, 4, 7 | syl3anc 1370 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β {π} β (π + {π})) |
9 | | vex 3477 |
. . . . 5
β’ π β V |
10 | 9 | snss 4789 |
. . . 4
β’ (π β (π + {π}) β {π} β (π + {π})) |
11 | 8, 10 | sylibr 233 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β π β (π + {π})) |
12 | | osumcllem.m |
. . 3
β’ π = (π + {π}) |
13 | 11, 12 | eleqtrrdi 2843 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β π β π) |
14 | 5, 6 | sspadd1 38990 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β (π + π)) |
15 | 14 | 3ad2ant1 1132 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β π β (π + π)) |
16 | | simp3 1137 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β Β¬ π β (π + π)) |
17 | 15, 16 | ssneldd 3985 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β Β¬ π β π) |
18 | | nelne1 3038 |
. 2
β’ ((π β π β§ Β¬ π β π) β π β π) |
19 | 13, 17, 18 | syl2anc 583 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π΄ β§ Β¬ π β (π + π)) β π β π) |