Step | Hyp | Ref
| Expression |
1 | | lhpex1.l |
. . . . 5
β’ β€ =
(leβπΎ) |
2 | | lhpex1.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
3 | | lhpex1.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 1, 2, 3 | lhpexle 38518 |
. . . 4
β’ ((πΎ β HL β§ π β π») β βπ β π΄ π β€ π) |
5 | | tru 1546 |
. . . . . 6
β’
β€ |
6 | 5 | jctr 526 |
. . . . 5
β’ (π β€ π β (π β€ π β§ β€)) |
7 | 6 | reximi 3084 |
. . . 4
β’
(βπ β
π΄ π β€ π β βπ β π΄ (π β€ π β§ β€)) |
8 | 4, 7 | syl 17 |
. . 3
β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ β€)) |
9 | | simpll 766 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β πΎ β HL) |
10 | | simprl 770 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β π β π΄) |
11 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
12 | 11, 3 | lhpbase 38511 |
. . . . . 6
β’ (π β π» β π β (BaseβπΎ)) |
13 | 12 | ad2antlr 726 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β π β (BaseβπΎ)) |
14 | | eqid 2733 |
. . . . . 6
β’
(ltβπΎ) =
(ltβπΎ) |
15 | 1, 14, 2, 3 | lhplt 38513 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β π(ltβπΎ)π) |
16 | 11, 14, 2 | 2atlt 37952 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β (BaseβπΎ)) β§ π(ltβπΎ)π) β βπ β π΄ (π β π β§ π(ltβπΎ)π)) |
17 | 9, 10, 13, 15, 16 | syl31anc 1374 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π΄ (π β π β§ π(ltβπΎ)π)) |
18 | | simp3r 1203 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β π(ltβπΎ)π) |
19 | | simp1ll 1237 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β πΎ β HL) |
20 | | simp2 1138 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β π β π΄) |
21 | | simp1lr 1238 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β π β π») |
22 | 1, 14 | pltle 18230 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π») β (π(ltβπΎ)π β π β€ π)) |
23 | 19, 20, 21, 22 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β (π(ltβπΎ)π β π β€ π)) |
24 | 18, 23 | mpd 15 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β π β€ π) |
25 | | trud 1552 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β β€) |
26 | | simp3l 1202 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β π β π) |
27 | 24, 25, 26 | 3jca 1129 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄ β§ (π β π β§ π(ltβπΎ)π)) β (π β€ π β§ β€ β§ π β π)) |
28 | 27 | 3expia 1122 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β§ π β π΄) β ((π β π β§ π(ltβπΎ)π) β (π β€ π β§ β€ β§ π β π))) |
29 | 28 | reximdva 3162 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β (βπ β π΄ (π β π β§ π(ltβπΎ)π) β βπ β π΄ (π β€ π β§ β€ β§ π β π))) |
30 | 17, 29 | mpd 15 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π΄ (π β€ π β§ β€ β§ π β π)) |
31 | 8, 30 | lhpexle1lem 38520 |
. 2
β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ β€ β§ π β π)) |
32 | | 3simpb 1150 |
. . 3
β’ ((π β€ π β§ β€ β§ π β π) β (π β€ π β§ π β π)) |
33 | 32 | reximi 3084 |
. 2
β’
(βπ β
π΄ (π β€ π β§ β€ β§ π β π) β βπ β π΄ (π β€ π β§ π β π)) |
34 | 31, 33 | syl 17 |
1
β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ π β π)) |