Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2733 |
. . 3
β’
(ltβπΎ) =
(ltβπΎ) |
3 | | eqid 2733 |
. . 3
β’
(0.βπΎ) =
(0.βπΎ) |
4 | | eqid 2733 |
. . 3
β’
(1.βπΎ) =
(1.βπΎ) |
5 | 1, 2, 3, 4 | hlhgt2 37898 |
. 2
β’ (πΎ β HL β βπ₯ β (BaseβπΎ)((0.βπΎ)(ltβπΎ)π₯ β§ π₯(ltβπΎ)(1.βπΎ))) |
6 | | simpl 484 |
. . . . . 6
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β πΎ β HL) |
7 | | hlop 37870 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β πΎ β OP) |
9 | 1, 3 | op0cl 37692 |
. . . . . . 7
β’ (πΎ β OP β
(0.βπΎ) β
(BaseβπΎ)) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β (0.βπΎ) β (BaseβπΎ)) |
11 | | simpr 486 |
. . . . . 6
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β π₯ β (BaseβπΎ)) |
12 | | eqid 2733 |
. . . . . . 7
β’
(leβπΎ) =
(leβπΎ) |
13 | | hl2atom.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
14 | 1, 12, 2, 13 | hlrelat1 37909 |
. . . . . 6
β’ ((πΎ β HL β§ (0.βπΎ) β (BaseβπΎ) β§ π₯ β (BaseβπΎ)) β ((0.βπΎ)(ltβπΎ)π₯ β βπ β π΄ (Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯))) |
15 | 6, 10, 11, 14 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β ((0.βπΎ)(ltβπΎ)π₯ β βπ β π΄ (Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯))) |
16 | 1, 4 | op1cl 37693 |
. . . . . . 7
β’ (πΎ β OP β
(1.βπΎ) β
(BaseβπΎ)) |
17 | 8, 16 | syl 17 |
. . . . . 6
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β (1.βπΎ) β (BaseβπΎ)) |
18 | 1, 12, 2, 13 | hlrelat1 37909 |
. . . . . 6
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ) β§ (1.βπΎ) β (BaseβπΎ)) β (π₯(ltβπΎ)(1.βπΎ) β βπ β π΄ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ)))) |
19 | 17, 18 | mpd3an3 1463 |
. . . . 5
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β (π₯(ltβπΎ)(1.βπΎ) β βπ β π΄ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ)))) |
20 | 15, 19 | anim12d 610 |
. . . 4
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β (((0.βπΎ)(ltβπΎ)π₯ β§ π₯(ltβπΎ)(1.βπΎ)) β (βπ β π΄ (Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ βπ β π΄ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ))))) |
21 | | reeanv 3216 |
. . . . 5
β’
(βπ β
π΄ βπ β π΄ ((Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ))) β (βπ β π΄ (Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ βπ β π΄ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ)))) |
22 | | nbrne2 5126 |
. . . . . . . 8
β’ ((π(leβπΎ)π₯ β§ Β¬ π(leβπΎ)π₯) β π β π) |
23 | 22 | ad2ant2lr 747 |
. . . . . . 7
β’ (((Β¬
π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ))) β π β π) |
24 | 23 | reximi 3084 |
. . . . . 6
β’
(βπ β
π΄ ((Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ))) β βπ β π΄ π β π) |
25 | 24 | reximi 3084 |
. . . . 5
β’
(βπ β
π΄ βπ β π΄ ((Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ))) β βπ β π΄ βπ β π΄ π β π) |
26 | 21, 25 | sylbir 234 |
. . . 4
β’
((βπ β
π΄ (Β¬ π(leβπΎ)(0.βπΎ) β§ π(leβπΎ)π₯) β§ βπ β π΄ (Β¬ π(leβπΎ)π₯ β§ π(leβπΎ)(1.βπΎ))) β βπ β π΄ βπ β π΄ π β π) |
27 | 20, 26 | syl6 35 |
. . 3
β’ ((πΎ β HL β§ π₯ β (BaseβπΎ)) β (((0.βπΎ)(ltβπΎ)π₯ β§ π₯(ltβπΎ)(1.βπΎ)) β βπ β π΄ βπ β π΄ π β π)) |
28 | 27 | rexlimdva 3149 |
. 2
β’ (πΎ β HL β (βπ₯ β (BaseβπΎ)((0.βπΎ)(ltβπΎ)π₯ β§ π₯(ltβπΎ)(1.βπΎ)) β βπ β π΄ βπ β π΄ π β π)) |
29 | 5, 28 | mpd 15 |
1
β’ (πΎ β HL β βπ β π΄ βπ β π΄ π β π) |