Step | Hyp | Ref
| Expression |
1 | | cdleme41.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | 1 | fvexi 6860 |
. 2
β’ π΅ β V |
3 | | nfv 1918 |
. . 3
β’
β²π (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) |
4 | | nfcsb1v 3884 |
. . . . 5
β’
β²π β¦π
/ π β¦π |
5 | | nfcv 2904 |
. . . . 5
β’
β²π
β¨ |
6 | | nfcv 2904 |
. . . . 5
β’
β²π (π β§ π) |
7 | 4, 5, 6 | nfov 7391 |
. . . 4
β’
β²π (β¦π
/ π β¦π β¨ (π β§ π)) |
8 | 7 | a1i 11 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β β²π (β¦π
/ π β¦π β¨ (π β§ π))) |
9 | | nfvd 1919 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β β²π (Β¬ π
β€ π β§ (π
β¨ (π β§ π)) = π)) |
10 | | cdleme41.o |
. . . . 5
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) |
11 | | cdleme41.f |
. . . . 5
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) |
12 | | eqid 2733 |
. . . . 5
β’
(β©π§
β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) |
13 | 10, 11, 12 | cdleme31fv1 38904 |
. . . 4
β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π))))) |
14 | 13 | 3ad2ant2 1135 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (πΉβπ) = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π))))) |
15 | | breq1 5112 |
. . . . . 6
β’ (π = π
β (π β€ π β π
β€ π)) |
16 | 15 | notbid 318 |
. . . . 5
β’ (π = π
β (Β¬ π β€ π β Β¬ π
β€ π)) |
17 | | oveq1 7368 |
. . . . . 6
β’ (π = π
β (π β¨ (π β§ π)) = (π
β¨ (π β§ π))) |
18 | 17 | eqeq1d 2735 |
. . . . 5
β’ (π = π
β ((π β¨ (π β§ π)) = π β (π
β¨ (π β§ π)) = π)) |
19 | 16, 18 | anbi12d 632 |
. . . 4
β’ (π = π
β ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β (Β¬ π
β€ π β§ (π
β¨ (π β§ π)) = π))) |
20 | 19 | adantl 483 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β§ π = π
) β ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β (Β¬ π
β€ π β§ (π
β¨ (π β§ π)) = π))) |
21 | | csbeq1a 3873 |
. . . . 5
β’ (π = π
β π = β¦π
/ π β¦π) |
22 | 21 | oveq1d 7376 |
. . . 4
β’ (π = π
β (π β¨ (π β§ π)) = (β¦π
/ π β¦π β¨ (π β§ π))) |
23 | 22 | adantl 483 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β§ π = π
) β (π β¨ (π β§ π)) = (β¦π
/ π β¦π β¨ (π β§ π))) |
24 | | simp1 1137 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
25 | | simp2l 1200 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β π β π΅) |
26 | | cdleme41.l |
. . . . 5
β’ β€ =
(leβπΎ) |
27 | | cdleme41.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
28 | | cdleme41.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
29 | | cdleme41.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
30 | | cdleme41.h |
. . . . 5
β’ π» = (LHypβπΎ) |
31 | | cdleme41.u |
. . . . 5
β’ π = ((π β¨ π) β§ π) |
32 | | cdleme41.d |
. . . . 5
β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) |
33 | | cdleme41.e |
. . . . 5
β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
34 | | cdleme41.g |
. . . . 5
β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) |
35 | | cdleme41.i |
. . . . 5
β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) |
36 | | cdleme41.n |
. . . . 5
β’ π = if(π β€ (π β¨ π), πΌ, π·) |
37 | 1, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 10, 11 | cdleme32fvcl 38953 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β (πΉβπ) β π΅) |
38 | 24, 25, 37 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (πΉβπ) β π΅) |
39 | | simp3ll 1245 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β π
β π΄) |
40 | | simp3lr 1246 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β Β¬ π
β€ π) |
41 | | simp3r 1203 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (π
β¨ (π β§ π)) = π) |
42 | 40, 41 | jca 513 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (Β¬ π
β€ π β§ (π
β¨ (π β§ π)) = π)) |
43 | 3, 8, 9, 14, 20, 23, 38, 39, 42 | riotasv2d 37469 |
. 2
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β§ π΅ β V) β (πΉβπ) = (β¦π
/ π β¦π β¨ (π β§ π))) |
44 | 2, 43 | mpan2 690 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (πΉβπ) = (β¦π
/ π β¦π β¨ (π β§ π))) |