Step | Hyp | Ref
| Expression |
1 | | hlclat 37823 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
2 | 1 | ad3antrrr 729 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π) β πΎ β CLat) |
3 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π) β π β π) |
4 | | simpllr 775 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π) β π β π΄) |
5 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
6 | | 2polss.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
7 | 5, 6 | atssbase 37755 |
. . . . . 6
β’ π΄ β (BaseβπΎ) |
8 | 4, 7 | sstrdi 3957 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π) β π β (BaseβπΎ)) |
9 | | eqid 2737 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
10 | | eqid 2737 |
. . . . . 6
β’
(lubβπΎ) =
(lubβπΎ) |
11 | 5, 9, 10 | lubel 18404 |
. . . . 5
β’ ((πΎ β CLat β§ π β π β§ π β (BaseβπΎ)) β π(leβπΎ)((lubβπΎ)βπ)) |
12 | 2, 3, 8, 11 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π) β π(leβπΎ)((lubβπΎ)βπ)) |
13 | 12 | ex 414 |
. . 3
β’ (((πΎ β HL β§ π β π΄) β§ π β π΄) β (π β π β π(leβπΎ)((lubβπΎ)βπ))) |
14 | 13 | ss2rabdv 4034 |
. 2
β’ ((πΎ β HL β§ π β π΄) β {π β π΄ β£ π β π} β {π β π΄ β£ π(leβπΎ)((lubβπΎ)βπ)}) |
15 | | sseqin2 4176 |
. . . . 5
β’ (π β π΄ β (π΄ β© π) = π) |
16 | 15 | biimpi 215 |
. . . 4
β’ (π β π΄ β (π΄ β© π) = π) |
17 | 16 | adantl 483 |
. . 3
β’ ((πΎ β HL β§ π β π΄) β (π΄ β© π) = π) |
18 | | dfin5 3919 |
. . 3
β’ (π΄ β© π) = {π β π΄ β£ π β π} |
19 | 17, 18 | eqtr3di 2792 |
. 2
β’ ((πΎ β HL β§ π β π΄) β π = {π β π΄ β£ π β π}) |
20 | | eqid 2737 |
. . . 4
β’
(pmapβπΎ) =
(pmapβπΎ) |
21 | | 2polss.p |
. . . 4
β’ β₯ =
(β₯πβπΎ) |
22 | 10, 6, 20, 21 | 2polvalN 38380 |
. . 3
β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯
βπ)) =
((pmapβπΎ)β((lubβπΎ)βπ))) |
23 | | sstr 3953 |
. . . . . 6
β’ ((π β π΄ β§ π΄ β (BaseβπΎ)) β π β (BaseβπΎ)) |
24 | 7, 23 | mpan2 690 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
25 | 5, 10 | clatlubcl 18393 |
. . . . 5
β’ ((πΎ β CLat β§ π β (BaseβπΎ)) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
26 | 1, 24, 25 | syl2an 597 |
. . . 4
β’ ((πΎ β HL β§ π β π΄) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
27 | 5, 9, 6, 20 | pmapval 38223 |
. . . 4
β’ ((πΎ β HL β§
((lubβπΎ)βπ) β (BaseβπΎ)) β ((pmapβπΎ)β((lubβπΎ)βπ)) = {π β π΄ β£ π(leβπΎ)((lubβπΎ)βπ)}) |
28 | 26, 27 | syldan 592 |
. . 3
β’ ((πΎ β HL β§ π β π΄) β ((pmapβπΎ)β((lubβπΎ)βπ)) = {π β π΄ β£ π(leβπΎ)((lubβπΎ)βπ)}) |
29 | 22, 28 | eqtrd 2777 |
. 2
β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯
βπ)) = {π β π΄ β£ π(leβπΎ)((lubβπΎ)βπ)}) |
30 | 14, 19, 29 | 3sstr4d 3992 |
1
β’ ((πΎ β HL β§ π β π΄) β π β ( β₯ β( β₯
βπ))) |