Step | Hyp | Ref
| Expression |
1 | | cdleme24.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cdleme24.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | cdleme24.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | cdleme24.m |
. . 3
β’ β§ =
(meetβπΎ) |
5 | | cdleme24.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
6 | | cdleme24.h |
. . 3
β’ π» = (LHypβπΎ) |
7 | | cdleme24.u |
. . 3
β’ π = ((π β¨ π) β§ π) |
8 | | cdleme24.f |
. . 3
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
9 | | cdleme24.n |
. . 3
β’ π = ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π ) β§ π))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | cdleme25a 38845 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π β π΅)) |
11 | | eqid 2737 |
. . 3
β’ ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
12 | | eqid 2737 |
. . 3
β’ ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π))) = ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π))) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11,
12 | cdleme24 38844 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π))))) |
14 | | breq1 5113 |
. . . . . 6
β’ (π = π‘ β (π β€ π β π‘ β€ π)) |
15 | 14 | notbid 318 |
. . . . 5
β’ (π = π‘ β (Β¬ π β€ π β Β¬ π‘ β€ π)) |
16 | | breq1 5113 |
. . . . . 6
β’ (π = π‘ β (π β€ (π β¨ π) β π‘ β€ (π β¨ π))) |
17 | 16 | notbid 318 |
. . . . 5
β’ (π = π‘ β (Β¬ π β€ (π β¨ π) β Β¬ π‘ β€ (π β¨ π))) |
18 | 15, 17 | anbi12d 632 |
. . . 4
β’ (π = π‘ β ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)))) |
19 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π‘ β (π β¨ π) = (π‘ β¨ π)) |
20 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π‘ β (π β¨ π ) = (π β¨ π‘)) |
21 | 20 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π = π‘ β ((π β¨ π ) β§ π) = ((π β¨ π‘) β§ π)) |
22 | 21 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π‘ β (π β¨ ((π β¨ π ) β§ π)) = (π β¨ ((π β¨ π‘) β§ π))) |
23 | 19, 22 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π‘ β ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) |
24 | 8, 23 | eqtrid 2789 |
. . . . . . 7
β’ (π = π‘ β πΉ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) |
25 | | oveq2 7370 |
. . . . . . . 8
β’ (π = π‘ β (π
β¨ π ) = (π
β¨ π‘)) |
26 | 25 | oveq1d 7377 |
. . . . . . 7
β’ (π = π‘ β ((π
β¨ π ) β§ π) = ((π
β¨ π‘) β§ π)) |
27 | 24, 26 | oveq12d 7380 |
. . . . . 6
β’ (π = π‘ β (πΉ β¨ ((π
β¨ π ) β§ π)) = (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π))) |
28 | 27 | oveq2d 7378 |
. . . . 5
β’ (π = π‘ β ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π ) β§ π))) = ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π)))) |
29 | 9, 28 | eqtrid 2789 |
. . . 4
β’ (π = π‘ β π = ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π)))) |
30 | 18, 29 | reusv3 5365 |
. . 3
β’
(βπ β
π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π β π΅) β (βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π)))) β βπ’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π))) |
31 | 30 | biimpd 228 |
. 2
β’
(βπ β
π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π β π΅) β (βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = ((π β¨ π) β§ (((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β¨ ((π
β¨ π‘) β§ π)))) β βπ’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π))) |
32 | 10, 13, 31 | sylc 65 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π β§ π
β€ (π β¨ π))) β βπ’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) |