Step | Hyp | Ref
| Expression |
1 | | cdleme26.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cdleme26.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | cdleme26.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | cdleme26.m |
. . 3
β’ β§ =
(meetβπΎ) |
5 | | cdleme26.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
6 | | cdleme26.h |
. . 3
β’ π» = (LHypβπΎ) |
7 | | cdleme27.u |
. . 3
β’ π = ((π β¨ π) β§ π) |
8 | | cdleme27.f |
. . 3
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
9 | | cdleme27.z |
. . 3
β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
10 | | cdleme27.n |
. . 3
β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
11 | | cdleme27.d |
. . 3
β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
12 | | cdleme27.c |
. . 3
β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | cdleme29ex 38866 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (πΆ β¨ (π β§ π)) β π΅)) |
14 | | eqid 2737 |
. . 3
β’ ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
15 | | eqid 2737 |
. . 3
β’ ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) |
16 | | eqid 2737 |
. . 3
β’
(β©π’
β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))) = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))) |
17 | | eqid 2737 |
. . 3
β’ if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) = if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 14, 15, 16, 17 | cdleme28 38865 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) β¨ (π β§ π)))) |
19 | | breq1 5113 |
. . . . . 6
β’ (π = π‘ β (π β€ π β π‘ β€ π)) |
20 | 19 | notbid 318 |
. . . . 5
β’ (π = π‘ β (Β¬ π β€ π β Β¬ π‘ β€ π)) |
21 | | oveq1 7369 |
. . . . . 6
β’ (π = π‘ β (π β¨ (π β§ π)) = (π‘ β¨ (π β§ π))) |
22 | 21 | eqeq1d 2739 |
. . . . 5
β’ (π = π‘ β ((π β¨ (π β§ π)) = π β (π‘ β¨ (π β§ π)) = π)) |
23 | 20, 22 | anbi12d 632 |
. . . 4
β’ (π = π‘ β ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π))) |
24 | 12 | oveq1i 7372 |
. . . . 5
β’ (πΆ β¨ (π β§ π)) = (if(π β€ (π β¨ π), π·, πΉ) β¨ (π β§ π)) |
25 | | breq1 5113 |
. . . . . . 7
β’ (π = π‘ β (π β€ (π β¨ π) β π‘ β€ (π β¨ π))) |
26 | | oveq1 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = π‘ β (π β¨ π§) = (π‘ β¨ π§)) |
27 | 26 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ (π = π‘ β ((π β¨ π§) β§ π) = ((π‘ β¨ π§) β§ π)) |
28 | 27 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π = π‘ β (π β¨ ((π β¨ π§) β§ π)) = (π β¨ ((π‘ β¨ π§) β§ π))) |
29 | 28 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = π‘ β ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))) |
30 | 10, 29 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ (π = π‘ β π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))) |
31 | 30 | eqeq2d 2748 |
. . . . . . . . . . 11
β’ (π = π‘ β (π’ = π β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))) |
32 | 31 | imbi2d 341 |
. . . . . . . . . 10
β’ (π = π‘ β (((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π) β ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))))) |
33 | 32 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = π‘ β (βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π) β βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))))) |
34 | 33 | riotabidv 7320 |
. . . . . . . 8
β’ (π = π‘ β (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))))) |
35 | 11, 34 | eqtrid 2789 |
. . . . . . 7
β’ (π = π‘ β π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π)))))) |
36 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π‘ β (π β¨ π) = (π‘ β¨ π)) |
37 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = π‘ β (π β¨ π ) = (π β¨ π‘)) |
38 | 37 | oveq1d 7377 |
. . . . . . . . . 10
β’ (π = π‘ β ((π β¨ π ) β§ π) = ((π β¨ π‘) β§ π)) |
39 | 38 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = π‘ β (π β¨ ((π β¨ π ) β§ π)) = (π β¨ ((π β¨ π‘) β§ π))) |
40 | 36, 39 | oveq12d 7380 |
. . . . . . . 8
β’ (π = π‘ β ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) |
41 | 8, 40 | eqtrid 2789 |
. . . . . . 7
β’ (π = π‘ β πΉ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) |
42 | 25, 35, 41 | ifbieq12d 4519 |
. . . . . 6
β’ (π = π‘ β if(π β€ (π β¨ π), π·, πΉ) = if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))))) |
43 | 42 | oveq1d 7377 |
. . . . 5
β’ (π = π‘ β (if(π β€ (π β¨ π), π·, πΉ) β¨ (π β§ π)) = (if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) β¨ (π β§ π))) |
44 | 24, 43 | eqtrid 2789 |
. . . 4
β’ (π = π‘ β (πΆ β¨ (π β§ π)) = (if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) β¨ (π β§ π))) |
45 | 23, 44 | reusv3 5365 |
. . 3
β’
(βπ β
π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (πΆ β¨ (π β§ π)) β π΅) β (βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) β¨ (π β§ π))) β βπ£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π))))) |
46 | 45 | biimpd 228 |
. 2
β’
(βπ β
π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (πΆ β¨ (π β§ π)) β π΅) β (βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (if(π‘ β€ (π β¨ π), (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))))), ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π)))) β¨ (π β§ π))) β βπ£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π))))) |
47 | 13, 18, 46 | sylc 65 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) |