Step | Hyp | Ref
| Expression |
1 | | simp13 1206 |
. . . 4
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β πΎ β AtLat) |
2 | | atlpos 37809 |
. . . 4
β’ (πΎ β AtLat β πΎ β Poset) |
3 | 1, 2 | syl 17 |
. . 3
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β πΎ β Poset) |
4 | | atlrelat1.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
5 | | atlrelat1.l |
. . . . 5
β’ β€ =
(leβπΎ) |
6 | | atlrelat1.s |
. . . . 5
β’ < =
(ltβπΎ) |
7 | 4, 5, 6 | pltnle 18232 |
. . . 4
β’ (((πΎ β Poset β§ π β π΅ β§ π β π΅) β§ π < π) β Β¬ π β€ π) |
8 | 7 | ex 414 |
. . 3
β’ ((πΎ β Poset β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
9 | 3, 8 | syld3an1 1411 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π < π β Β¬ π β€ π)) |
10 | | iman 403 |
. . . . . . 7
β’ ((π β€ π β π β€ π) β Β¬ (π β€ π β§ Β¬ π β€ π)) |
11 | | ancom 462 |
. . . . . . 7
β’ ((π β€ π β§ Β¬ π β€ π) β (Β¬ π β€ π β§ π β€ π)) |
12 | 10, 11 | xchbinx 334 |
. . . . . 6
β’ ((π β€ π β π β€ π) β Β¬ (Β¬ π β€ π β§ π β€ π)) |
13 | 12 | ralbii 3093 |
. . . . 5
β’
(βπ β
π΄ (π β€ π β π β€ π) β βπ β π΄ Β¬ (Β¬ π β€ π β§ π β€ π)) |
14 | | atlrelat1.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
15 | 4, 5, 14 | atlatle 37828 |
. . . . . . 7
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) |
16 | 15 | 3com23 1127 |
. . . . . 6
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) |
17 | 16 | biimprd 248 |
. . . . 5
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (βπ β π΄ (π β€ π β π β€ π) β π β€ π)) |
18 | 13, 17 | biimtrrid 242 |
. . . 4
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (βπ β π΄ Β¬ (Β¬ π β€ π β§ π β€ π) β π β€ π)) |
19 | 18 | con3d 152 |
. . 3
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β Β¬ βπ β π΄ Β¬ (Β¬ π β€ π β§ π β€ π))) |
20 | | dfrex2 3073 |
. . 3
β’
(βπ β
π΄ (Β¬ π β€ π β§ π β€ π) β Β¬ βπ β π΄ Β¬ (Β¬ π β€ π β§ π β€ π)) |
21 | 19, 20 | syl6ibr 252 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) |
22 | 9, 21 | syld 47 |
1
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) |