Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β πΎ β HL) |
2 | | simp12 1205 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΄) |
3 | | simp13 1206 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΄) |
4 | | simp2l 1200 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΅) |
5 | | simp2r 1201 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β π β π) |
6 | | simp31 1210 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β ππΆ 1 ) |
7 | | simp32 1211 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β Β¬ π β€ π) |
8 | | cdlemb.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
9 | | cdlemb.l |
. . . . 5
β’ β€ =
(leβπΎ) |
10 | | cdlemb.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
11 | | eqid 2733 |
. . . . 5
β’
(meetβπΎ) =
(meetβπΎ) |
12 | | cdlemb.u |
. . . . 5
β’ 1 =
(1.βπΎ) |
13 | | cdlemb.c |
. . . . 5
β’ πΆ = ( β βπΎ) |
14 | | cdlemb.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
15 | 8, 9, 10, 11, 12, 13, 14 | 1cvrat 37985 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β π β§ ππΆ 1 β§ Β¬ π β€ π)) β ((π β¨ π)(meetβπΎ)π) β π΄) |
16 | 1, 2, 3, 4, 5, 6, 7, 15 | syl133anc 1394 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β ((π β¨ π)(meetβπΎ)π) β π΄) |
17 | 1 | hllatd 37872 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β πΎ β Lat) |
18 | 8, 14 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
19 | 2, 18 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΅) |
20 | 8, 14 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
21 | 3, 20 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΅) |
22 | 8, 10 | latjcl 18333 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
23 | 17, 19, 21, 22 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β (π β¨ π) β π΅) |
24 | 8, 9, 11 | latmle2 18359 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π)(meetβπΎ)π) β€ π) |
25 | 17, 23, 4, 24 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β ((π β¨ π)(meetβπΎ)π) β€ π) |
26 | | eqid 2733 |
. . . . 5
β’
(ltβπΎ) =
(ltβπΎ) |
27 | 8, 9, 26, 12, 13, 14 | 1cvratlt 37983 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π)(meetβπΎ)π) β π΄ β§ π β π΅) β§ (ππΆ 1 β§ ((π β¨ π)(meetβπΎ)π) β€ π)) β ((π β¨ π)(meetβπΎ)π)(ltβπΎ)π) |
28 | 1, 16, 4, 6, 25, 27 | syl32anc 1379 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β ((π β¨ π)(meetβπΎ)π)(ltβπΎ)π) |
29 | 8, 26, 14 | 2atlt 37948 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π)(meetβπΎ)π) β π΄ β§ π β π΅) β§ ((π β¨ π)(meetβπΎ)π)(ltβπΎ)π) β βπ’ β π΄ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π)) |
30 | 1, 16, 4, 28, 29 | syl31anc 1374 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β βπ’ β π΄ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π)) |
31 | | simpl11 1249 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β πΎ β HL) |
32 | | simpl12 1250 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β π β π΄) |
33 | | simprl 770 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β π’ β π΄) |
34 | | simpl32 1256 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β Β¬ π β€ π) |
35 | | simprrr 781 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β π’(ltβπΎ)π) |
36 | | simpl2l 1227 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β π β π΅) |
37 | 9, 26 | pltle 18227 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π’ β π΄ β§ π β π΅) β (π’(ltβπΎ)π β π’ β€ π)) |
38 | 31, 33, 36, 37 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β (π’(ltβπΎ)π β π’ β€ π)) |
39 | 35, 38 | mpd 15 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β π’ β€ π) |
40 | | breq1 5109 |
. . . . . . 7
β’ (π = π’ β (π β€ π β π’ β€ π)) |
41 | 39, 40 | syl5ibrcom 247 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β (π = π’ β π β€ π)) |
42 | 41 | necon3bd 2954 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β (Β¬ π β€ π β π β π’)) |
43 | 34, 42 | mpd 15 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β π β π’) |
44 | 9, 10, 14 | hlsupr 37895 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π’ β π΄) β§ π β π’) β βπ β π΄ (π β π β§ π β π’ β§ π β€ (π β¨ π’))) |
45 | 31, 32, 33, 43, 44 | syl31anc 1374 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β βπ β π΄ (π β π β§ π β π’ β§ π β€ (π β¨ π’))) |
46 | | eqid 2733 |
. . . . . . . 8
β’ ((π β¨ π)(meetβπΎ)π) = ((π β¨ π)(meetβπΎ)π) |
47 | 8, 9, 10, 12, 13, 14, 26, 11, 46 | cdlemblem 38302 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π)) β§ (π β π΄ β§ (π β π β§ π β π’ β§ π β€ (π β¨ π’)))) β (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) |
48 | 47 | 3exp 1120 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β ((π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π)) β ((π β π΄ β§ (π β π β§ π β π’ β§ π β€ (π β¨ π’))) β (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))))) |
49 | 48 | exp4a 433 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β ((π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π)) β (π β π΄ β ((π β π β§ π β π’ β§ π β€ (π β¨ π’)) β (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)))))) |
50 | 49 | imp 408 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β (π β π΄ β ((π β π β§ π β π’ β§ π β€ (π β¨ π’)) β (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))))) |
51 | 50 | reximdvai 3159 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β (βπ β π΄ (π β π β§ π β π’ β§ π β€ (π β¨ π’)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)))) |
52 | 45, 51 | mpd 15 |
. 2
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β§ (π’ β π΄ β§ (π’ β ((π β¨ π)(meetβπΎ)π) β§ π’(ltβπΎ)π))) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) |
53 | 30, 52 | rexlimddv 3155 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β π) β§ (ππΆ 1 β§ Β¬ π β€ π β§ Β¬ π β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) |