Step | Hyp | Ref
| Expression |
1 | | hlhgt4.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
3 | | hlhgt4.s |
. . 3
β’ < =
(ltβπΎ) |
4 | | eqid 2733 |
. . 3
β’
(joinβπΎ) =
(joinβπΎ) |
5 | | hlhgt4.z |
. . 3
β’ 0 =
(0.βπΎ) |
6 | | hlhgt4.u |
. . 3
β’ 1 =
(1.βπΎ) |
7 | | eqid 2733 |
. . 3
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
8 | 1, 2, 3, 4, 5, 6, 7 | ishlat2 38223 |
. 2
β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§
(βπ₯ β
(AtomsβπΎ)βπ¦ β (AtomsβπΎ)((π₯ β π¦ β βπ§ β (AtomsβπΎ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπΎ)(π₯(joinβπΎ)π¦))) β§ βπ§ β π΅ ((Β¬ π₯(leβπΎ)π§ β§ π₯(leβπΎ)(π§(joinβπΎ)π¦)) β π¦(leβπΎ)(π§(joinβπΎ)π₯))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))))) |
9 | | simprr 772 |
. 2
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§
(βπ₯ β
(AtomsβπΎ)βπ¦ β (AtomsβπΎ)((π₯ β π¦ β βπ§ β (AtomsβπΎ)(π§ β π₯ β§ π§ β π¦ β§ π§(leβπΎ)(π₯(joinβπΎ)π¦))) β§ βπ§ β π΅ ((Β¬ π₯(leβπΎ)π§ β§ π₯(leβπΎ)(π§(joinβπΎ)π¦)) β π¦(leβπΎ)(π§(joinβπΎ)π₯))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 )))) β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))) |
10 | 8, 9 | sylbi 216 |
1
β’ (πΎ β HL β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (( 0 < π₯ β§ π₯ < π¦) β§ (π¦ < π§ β§ π§ < 1 ))) |