Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β πΎ β HL) |
2 | | simp11r 1286 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β π β π») |
3 | | simp12 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
4 | | simp13 1206 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
5 | | simp3l1 1279 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β π β π) |
6 | | cdleme26.l |
. . . 4
β’ β€ =
(leβπΎ) |
7 | | cdleme26.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
8 | | cdleme26.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
9 | | cdleme26.h |
. . . 4
β’ π» = (LHypβπΎ) |
10 | 6, 7, 8, 9 | cdlemb2 38533 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β βπ§ β π΄ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) |
11 | 1, 2, 3, 4, 5, 10 | syl221anc 1382 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β βπ§ β π΄ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) |
12 | | nfv 1918 |
. . 3
β’
β²π§(((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) |
13 | | cdleme26e.i |
. . . . 5
β’ πΌ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
14 | | nfra1 3270 |
. . . . . 6
β’
β²π§βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π) |
15 | | nfcv 2908 |
. . . . . 6
β’
β²π§π΅ |
16 | 14, 15 | nfriota 7331 |
. . . . 5
β’
β²π§(β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
17 | 13, 16 | nfcxfr 2906 |
. . . 4
β’
β²π§πΌ |
18 | | nfcv 2908 |
. . . 4
β’
β²π§
β€ |
19 | | cdleme26e.e |
. . . . . 6
β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
20 | | nfra1 3270 |
. . . . . . 7
β’
β²π§βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π) |
21 | 20, 15 | nfriota 7331 |
. . . . . 6
β’
β²π§(β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) |
22 | 19, 21 | nfcxfr 2906 |
. . . . 5
β’
β²π§πΈ |
23 | | nfcv 2908 |
. . . . 5
β’
β²π§
β¨ |
24 | | nfcv 2908 |
. . . . 5
β’
β²π§π |
25 | 22, 23, 24 | nfov 7392 |
. . . 4
β’
β²π§(πΈ β¨ π) |
26 | 17, 18, 25 | nfbr 5157 |
. . 3
β’
β²π§ πΌ β€ (πΈ β¨ π) |
27 | | simp111 1303 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (πΎ β HL β§ π β π»)) |
28 | | simp112 1304 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
29 | | simp113 1305 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
30 | | simp121 1306 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
31 | | simp122 1307 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
32 | | simp123 1308 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β π΄ β§ π β€ π)) |
33 | | simp13l 1289 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π))) |
34 | | simp13r 1290 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π β¨ π) = (π β¨ π)) |
35 | | simp3r 1203 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β Β¬ π§ β€ (π β¨ π)) |
36 | 34, 35 | jca 513 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β ((π β¨ π) = (π β¨ π) β§ Β¬ π§ β€ (π β¨ π))) |
37 | | simp2 1138 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β π§ β π΄) |
38 | | simp3l 1202 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β Β¬ π§ β€ π) |
39 | 37, 38 | jca 513 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β (π§ β π΄ β§ Β¬ π§ β€ π)) |
40 | | cdleme26.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
41 | | cdleme26.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
42 | | cdleme26e.u |
. . . . . 6
β’ π = ((π β¨ π) β§ π) |
43 | | cdleme26e.f |
. . . . . 6
β’ πΉ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) |
44 | | cdleme26e.n |
. . . . . 6
β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) |
45 | | cdleme26e.o |
. . . . . 6
β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) |
46 | 40, 6, 7, 41, 8, 9,
42, 43, 44, 45, 13, 19 | cdleme26e 38851 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π β¨ π) = (π β¨ π) β§ Β¬ π§ β€ (π β¨ π)) β§ (π§ β π΄ β§ Β¬ π§ β€ π))) β πΌ β€ (πΈ β¨ π)) |
47 | 27, 28, 29, 30, 31, 32, 33, 36, 39, 46 | syl333anc 1403 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β§ π§ β π΄ β§ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π))) β πΌ β€ (πΈ β¨ π)) |
48 | 47 | 3exp 1120 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β (π§ β π΄ β ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β πΌ β€ (πΈ β¨ π)))) |
49 | 12, 26, 48 | rexlimd 3252 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β (βπ§ β π΄ (Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β πΌ β€ (πΈ β¨ π))) |
50 | 11, 49 | mpd 15 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β πΌ β€ (πΈ β¨ π)) |