Step | Hyp | Ref
| Expression |
1 | | hlpos 38236 |
. . . . 5
β’ (πΎ β HL β πΎ β Poset) |
2 | | pmaple.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
3 | | eqid 2733 |
. . . . . . . . . 10
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | 2, 3 | atbase 38159 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β π΅) |
5 | | pmaple.l |
. . . . . . . . . . . . . . 15
β’ β€ =
(leβπΎ) |
6 | 2, 5 | postr 18273 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Poset β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ π)) |
7 | 6 | exp4b 432 |
. . . . . . . . . . . . 13
β’ (πΎ β Poset β ((π β π΅ β§ π β π΅ β§ π β π΅) β (π β€ π β (π β€ π β π β€ π)))) |
8 | 7 | 3expd 1354 |
. . . . . . . . . . . 12
β’ (πΎ β Poset β (π β π΅ β (π β π΅ β (π β π΅ β (π β€ π β (π β€ π β π β€ π)))))) |
9 | 8 | com23 86 |
. . . . . . . . . . 11
β’ (πΎ β Poset β (π β π΅ β (π β π΅ β (π β π΅ β (π β€ π β (π β€ π β π β€ π)))))) |
10 | 9 | com34 91 |
. . . . . . . . . 10
β’ (πΎ β Poset β (π β π΅ β (π β π΅ β (π β π΅ β (π β€ π β (π β€ π β π β€ π)))))) |
11 | 10 | 3imp 1112 |
. . . . . . . . 9
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β π΅ β (π β€ π β (π β€ π β π β€ π)))) |
12 | 4, 11 | syl5 34 |
. . . . . . . 8
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β (AtomsβπΎ) β (π β€ π β (π β€ π β π β€ π)))) |
13 | 12 | com34 91 |
. . . . . . 7
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β (AtomsβπΎ) β (π β€ π β (π β€ π β π β€ π)))) |
14 | 13 | com23 86 |
. . . . . 6
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β€ π β (π β (AtomsβπΎ) β (π β€ π β π β€ π)))) |
15 | 14 | ralrimdv 3153 |
. . . . 5
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β (AtomsβπΎ)(π β€ π β π β€ π))) |
16 | 1, 15 | syl3an1 1164 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β (AtomsβπΎ)(π β€ π β π β€ π))) |
17 | | ss2rab 4069 |
. . . 4
β’ ({π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π} β βπ β (AtomsβπΎ)(π β€ π β π β€ π)) |
18 | 16, 17 | syl6ibr 252 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β {π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π})) |
19 | | hlclat 38228 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
20 | | ssrab2 4078 |
. . . . . . . . 9
β’ {π β (AtomsβπΎ) β£ π β€ π} β (AtomsβπΎ) |
21 | 2, 3 | atssbase 38160 |
. . . . . . . . 9
β’
(AtomsβπΎ)
β π΅ |
22 | 20, 21 | sstri 3992 |
. . . . . . . 8
β’ {π β (AtomsβπΎ) β£ π β€ π} β π΅ |
23 | | eqid 2733 |
. . . . . . . . 9
β’
(lubβπΎ) =
(lubβπΎ) |
24 | 2, 5, 23 | lubss 18466 |
. . . . . . . 8
β’ ((πΎ β CLat β§ {π β (AtomsβπΎ) β£ π β€ π} β π΅ β§ {π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π}) β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β€ ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π})) |
25 | 22, 24 | mp3an2 1450 |
. . . . . . 7
β’ ((πΎ β CLat β§ {π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π}) β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β€ ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π})) |
26 | 25 | ex 414 |
. . . . . 6
β’ (πΎ β CLat β ({π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π} β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β€ ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}))) |
27 | 19, 26 | syl 17 |
. . . . 5
β’ (πΎ β HL β ({π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π} β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β€ ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}))) |
28 | 27 | 3ad2ant1 1134 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ({π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π} β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β€ ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}))) |
29 | | hlomcmat 38235 |
. . . . . . 7
β’ (πΎ β HL β (πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat)) |
30 | 29 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat)) |
31 | | simp2 1138 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
32 | 2, 5, 23, 3 | atlatmstc 38189 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅) β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) = π) |
33 | 30, 31, 32 | syl2anc 585 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) = π) |
34 | | simp3 1139 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
35 | 2, 5, 23, 3 | atlatmstc 38189 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅) β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) = π) |
36 | 30, 34, 35 | syl2anc 585 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) = π) |
37 | 33, 36 | breq12d 5162 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β€ ((lubβπΎ)β{π β (AtomsβπΎ) β£ π β€ π}) β π β€ π)) |
38 | 28, 37 | sylibd 238 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ({π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π} β π β€ π)) |
39 | 18, 38 | impbid 211 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β {π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π})) |
40 | | pmaple.m |
. . . . 5
β’ π = (pmapβπΎ) |
41 | 2, 5, 3, 40 | pmapval 38628 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (πβπ) = {π β (AtomsβπΎ) β£ π β€ π}) |
42 | 41 | 3adant3 1133 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβπ) = {π β (AtomsβπΎ) β£ π β€ π}) |
43 | 2, 5, 3, 40 | pmapval 38628 |
. . . 4
β’ ((πΎ β HL β§ π β π΅) β (πβπ) = {π β (AtomsβπΎ) β£ π β€ π}) |
44 | 43 | 3adant2 1132 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβπ) = {π β (AtomsβπΎ) β£ π β€ π}) |
45 | 42, 44 | sseq12d 4016 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((πβπ) β (πβπ) β {π β (AtomsβπΎ) β£ π β€ π} β {π β (AtomsβπΎ) β£ π β€ π})) |
46 | 39, 45 | bitr4d 282 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β (πβπ) β (πβπ))) |