Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β HL) |
2 | | simpl2 1192 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
3 | | simpr 485 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) |
4 | 3 | snssd 4812 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β {π} β π) |
5 | | osumcllem.u |
. . . . . 6
β’ π = ( β₯ β( β₯
β(π + π))) |
6 | | osumcllem.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
7 | | osumcllem.p |
. . . . . . . . . 10
β’ + =
(+πβπΎ) |
8 | 6, 7 | paddssat 38777 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π + π) β π΄) |
9 | 8 | adantr 481 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π + π) β π΄) |
10 | | osumcllem.o |
. . . . . . . . 9
β’ β₯ =
(β₯πβπΎ) |
11 | 6, 10 | polssatN 38871 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π + π) β π΄) β ( β₯ β(π + π)) β π΄) |
12 | 1, 9, 11 | syl2anc 584 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β ( β₯ β(π + π)) β π΄) |
13 | 6, 10 | polssatN 38871 |
. . . . . . 7
β’ ((πΎ β HL β§ ( β₯
β(π + π)) β π΄) β ( β₯ β( β₯
β(π + π))) β π΄) |
14 | 1, 12, 13 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β ( β₯ β( β₯
β(π + π))) β π΄) |
15 | 5, 14 | eqsstrid 4030 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
16 | 4, 15 | sstrd 3992 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β {π} β π΄) |
17 | 6, 7 | sspadd1 38778 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ {π} β π΄) β π β (π + {π})) |
18 | 1, 2, 16, 17 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β (π + {π})) |
19 | | osumcllem.m |
. . 3
β’ π = (π + {π}) |
20 | 18, 19 | sseqtrrdi 4033 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) |
21 | | osumcllem.l |
. . 3
β’ β€ =
(leβπΎ) |
22 | | osumcllem.j |
. . 3
β’ β¨ =
(joinβπΎ) |
23 | | osumcllem.c |
. . 3
β’ πΆ = (PSubClβπΎ) |
24 | 21, 22, 6, 7, 10, 23, 19, 5 | osumcllem1N 38919 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β© π) = π) |
25 | 20, 24 | sseqtrrd 4023 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β (π β© π)) |