Step | Hyp | Ref
| Expression |
1 | | hlsuprexch.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | hlsuprexch.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | eqid 2733 |
. . . . 5
β’
(ltβπΎ) =
(ltβπΎ) |
4 | | hlsuprexch.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
5 | | eqid 2733 |
. . . . 5
β’
(0.βπΎ) =
(0.βπΎ) |
6 | | eqid 2733 |
. . . . 5
β’
(1.βπΎ) =
(1.βπΎ) |
7 | | hlsuprexch.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
8 | 1, 2, 3, 4, 5, 6, 7 | ishlat2 37861 |
. . . 4
β’ (πΎ β HL β ((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§
(βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (((0.βπΎ)(ltβπΎ)π₯ β§ π₯(ltβπΎ)π¦) β§ (π¦(ltβπΎ)π§ β§ π§(ltβπΎ)(1.βπΎ)))))) |
9 | | simprl 770 |
. . . 4
β’ (((πΎ β OML β§ πΎ β CLat β§ πΎ β AtLat) β§
(βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (((0.βπΎ)(ltβπΎ)π₯ β§ π₯(ltβπΎ)π¦) β§ (π¦(ltβπΎ)π§ β§ π§(ltβπΎ)(1.βπΎ))))) β βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯)))) |
10 | 8, 9 | sylbi 216 |
. . 3
β’ (πΎ β HL β βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯)))) |
11 | | neeq1 3003 |
. . . . . 6
β’ (π₯ = π β (π₯ β π¦ β π β π¦)) |
12 | | neeq2 3004 |
. . . . . . . 8
β’ (π₯ = π β (π§ β π₯ β π§ β π)) |
13 | | oveq1 7365 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β¨ π¦) = (π β¨ π¦)) |
14 | 13 | breq2d 5118 |
. . . . . . . 8
β’ (π₯ = π β (π§ β€ (π₯ β¨ π¦) β π§ β€ (π β¨ π¦))) |
15 | 12, 14 | 3anbi13d 1439 |
. . . . . . 7
β’ (π₯ = π β ((π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)) β (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦)))) |
16 | 15 | rexbidv 3172 |
. . . . . 6
β’ (π₯ = π β (βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦)) β βπ§ β π΄ (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦)))) |
17 | 11, 16 | imbi12d 345 |
. . . . 5
β’ (π₯ = π β ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β (π β π¦ β βπ§ β π΄ (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦))))) |
18 | | breq1 5109 |
. . . . . . . . 9
β’ (π₯ = π β (π₯ β€ π§ β π β€ π§)) |
19 | 18 | notbid 318 |
. . . . . . . 8
β’ (π₯ = π β (Β¬ π₯ β€ π§ β Β¬ π β€ π§)) |
20 | | breq1 5109 |
. . . . . . . 8
β’ (π₯ = π β (π₯ β€ (π§ β¨ π¦) β π β€ (π§ β¨ π¦))) |
21 | 19, 20 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = π β ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β (Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)))) |
22 | | oveq2 7366 |
. . . . . . . 8
β’ (π₯ = π β (π§ β¨ π₯) = (π§ β¨ π)) |
23 | 22 | breq2d 5118 |
. . . . . . 7
β’ (π₯ = π β (π¦ β€ (π§ β¨ π₯) β π¦ β€ (π§ β¨ π))) |
24 | 21, 23 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π β (((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯)) β ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π)))) |
25 | 24 | ralbidv 3171 |
. . . . 5
β’ (π₯ = π β (βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯)) β βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π)))) |
26 | 17, 25 | anbi12d 632 |
. . . 4
β’ (π₯ = π β (((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) β ((π β π¦ β βπ§ β π΄ (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π))))) |
27 | | neeq2 3004 |
. . . . . 6
β’ (π¦ = π β (π β π¦ β π β π)) |
28 | | neeq2 3004 |
. . . . . . . 8
β’ (π¦ = π β (π§ β π¦ β π§ β π)) |
29 | | oveq2 7366 |
. . . . . . . . 9
β’ (π¦ = π β (π β¨ π¦) = (π β¨ π)) |
30 | 29 | breq2d 5118 |
. . . . . . . 8
β’ (π¦ = π β (π§ β€ (π β¨ π¦) β π§ β€ (π β¨ π))) |
31 | 28, 30 | 3anbi23d 1440 |
. . . . . . 7
β’ (π¦ = π β ((π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦)) β (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π)))) |
32 | 31 | rexbidv 3172 |
. . . . . 6
β’ (π¦ = π β (βπ§ β π΄ (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦)) β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π)))) |
33 | 27, 32 | imbi12d 345 |
. . . . 5
β’ (π¦ = π β ((π β π¦ β βπ§ β π΄ (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦))) β (π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))))) |
34 | | oveq2 7366 |
. . . . . . . . 9
β’ (π¦ = π β (π§ β¨ π¦) = (π§ β¨ π)) |
35 | 34 | breq2d 5118 |
. . . . . . . 8
β’ (π¦ = π β (π β€ (π§ β¨ π¦) β π β€ (π§ β¨ π))) |
36 | 35 | anbi2d 630 |
. . . . . . 7
β’ (π¦ = π β ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β (Β¬ π β€ π§ β§ π β€ (π§ β¨ π)))) |
37 | | breq1 5109 |
. . . . . . 7
β’ (π¦ = π β (π¦ β€ (π§ β¨ π) β π β€ (π§ β¨ π))) |
38 | 36, 37 | imbi12d 345 |
. . . . . 6
β’ (π¦ = π β (((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π)) β ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π)))) |
39 | 38 | ralbidv 3171 |
. . . . 5
β’ (π¦ = π β (βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π)) β βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π)))) |
40 | 33, 39 | anbi12d 632 |
. . . 4
β’ (π¦ = π β (((π β π¦ β βπ§ β π΄ (π§ β π β§ π§ β π¦ β§ π§ β€ (π β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π))) β ((π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π))))) |
41 | 26, 40 | rspc2v 3589 |
. . 3
β’ ((π β π΄ β§ π β π΄) β (βπ₯ β π΄ βπ¦ β π΄ ((π₯ β π¦ β βπ§ β π΄ (π§ β π₯ β§ π§ β π¦ β§ π§ β€ (π₯ β¨ π¦))) β§ βπ§ β π΅ ((Β¬ π₯ β€ π§ β§ π₯ β€ (π§ β¨ π¦)) β π¦ β€ (π§ β¨ π₯))) β ((π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π))))) |
42 | 10, 41 | mpan9 508 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄)) β ((π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π)))) |
43 | 42 | 3impb 1116 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β π β βπ§ β π΄ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π))) β§ βπ§ β π΅ ((Β¬ π β€ π§ β§ π β€ (π§ β¨ π)) β π β€ (π§ β¨ π)))) |