Step | Hyp | Ref
| Expression |
1 | | ltrnset.l |
. . 3
β’ β€ =
(leβπΎ) |
2 | | ltrnset.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | ltrnset.m |
. . 3
β’ β§ =
(meetβπΎ) |
4 | | ltrnset.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
5 | | ltrnset.h |
. . 3
β’ π» = (LHypβπΎ) |
6 | | ltrnset.d |
. . 3
β’ π· = ((LDilβπΎ)βπ) |
7 | | ltrnset.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | isltrn 38632 |
. 2
β’ ((πΎ β π΅ β§ π β π») β (πΉ β π β (πΉ β π· β§ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))))) |
9 | | 3simpa 1149 |
. . . . . 6
β’ ((Β¬
π β€ π β§ Β¬ π β€ π β§ π β π) β (Β¬ π β€ π β§ Β¬ π β€ π)) |
10 | 9 | imim1i 63 |
. . . . 5
β’ (((Β¬
π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
11 | | 3anass 1096 |
. . . . . . . . 9
β’ ((π β π β§ Β¬ π β€ π β§ Β¬ π β€ π) β (π β π β§ (Β¬ π β€ π β§ Β¬ π β€ π))) |
12 | | 3anrot 1101 |
. . . . . . . . 9
β’ ((π β π β§ Β¬ π β€ π β§ Β¬ π β€ π) β (Β¬ π β€ π β§ Β¬ π β€ π β§ π β π)) |
13 | | df-ne 2941 |
. . . . . . . . . 10
β’ (π β π β Β¬ π = π) |
14 | 13 | anbi1i 625 |
. . . . . . . . 9
β’ ((π β π β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β (Β¬ π = π β§ (Β¬ π β€ π β§ Β¬ π β€ π))) |
15 | 11, 12, 14 | 3bitr3i 301 |
. . . . . . . 8
β’ ((Β¬
π β€ π β§ Β¬ π β€ π β§ π β π) β (Β¬ π = π β§ (Β¬ π β€ π β§ Β¬ π β€ π))) |
16 | 15 | imbi1i 350 |
. . . . . . 7
β’ (((Β¬
π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β ((Β¬ π = π β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
17 | | impexp 452 |
. . . . . . 7
β’ (((Β¬
π = π β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β (Β¬ π = π β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)))) |
18 | 16, 17 | bitri 275 |
. . . . . 6
β’ (((Β¬
π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β (Β¬ π = π β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)))) |
19 | | id 22 |
. . . . . . . . . 10
β’ (π = π β π = π) |
20 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
21 | 19, 20 | oveq12d 7379 |
. . . . . . . . 9
β’ (π = π β (π β¨ (πΉβπ)) = (π β¨ (πΉβπ))) |
22 | 21 | oveq1d 7376 |
. . . . . . . 8
β’ (π = π β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) |
23 | 22 | a1d 25 |
. . . . . . 7
β’ (π = π β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
24 | | pm2.61 191 |
. . . . . . 7
β’ ((π = π β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) β ((Β¬ π = π β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)))) |
25 | 23, 24 | ax-mp 5 |
. . . . . 6
β’ ((Β¬
π = π β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
26 | 18, 25 | sylbi 216 |
. . . . 5
β’ (((Β¬
π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
27 | 10, 26 | impbii 208 |
. . . 4
β’ (((Β¬
π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
28 | 27 | 2ralbii 3124 |
. . 3
β’
(βπ β
π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) β βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) |
29 | 28 | anbi2i 624 |
. 2
β’ ((πΉ β π· β§ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))) β (πΉ β π· β§ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)))) |
30 | 8, 29 | bitrdi 287 |
1
β’ ((πΎ β π΅ β§ π β π») β (πΉ β π β (πΉ β π· β§ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))))) |