Step | Hyp | Ref
| Expression |
1 | | 4thatlem0.c |
. . . 4
β’ πΆ = ((π β¨ π) β§ (π β¨ π)) |
2 | | 4thatlem.ph |
. . . . . 6
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π
β π΄ β§ Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
)) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) |
3 | 2 | 4atexlemkl 39467 |
. . . . 5
β’ (π β πΎ β Lat) |
4 | | 4thatlem0.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
5 | | 4thatlem0.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
6 | 2, 4, 5 | 4atexlemqtb 39471 |
. . . . 5
β’ (π β (π β¨ π) β (BaseβπΎ)) |
7 | 2, 4, 5 | 4atexlempsb 39470 |
. . . . 5
β’ (π β (π β¨ π) β (BaseβπΎ)) |
8 | | eqid 2727 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
9 | | 4thatlem0.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
10 | | 4thatlem0.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
11 | 8, 9, 10 | latmle1 18447 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
12 | 3, 6, 7, 11 | syl3anc 1369 |
. . . 4
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
13 | 1, 12 | eqbrtrid 5177 |
. . 3
β’ (π β πΆ β€ (π β¨ π)) |
14 | | simp13r 1287 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π
β π΄ β§ Β¬ π
β€ π β§ (π β¨ π
) = (π β¨ π
)) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ π) |
15 | 2, 14 | sylbi 216 |
. . . 4
β’ (π β Β¬ π β€ π) |
16 | 2 | 4atexlemkc 39468 |
. . . . . 6
β’ (π β πΎ β CvLat) |
17 | | 4thatlem0.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
18 | | 4thatlem0.u |
. . . . . . 7
β’ π = ((π β¨ π) β§ π) |
19 | | 4thatlem0.v |
. . . . . . 7
β’ π = ((π β¨ π) β§ π) |
20 | 2, 9, 4, 10, 5, 17, 18, 19 | 4atexlemv 39475 |
. . . . . 6
β’ (π β π β π΄) |
21 | 2 | 4atexlemq 39461 |
. . . . . 6
β’ (π β π β π΄) |
22 | 2 | 4atexlemt 39463 |
. . . . . 6
β’ (π β π β π΄) |
23 | 2, 9, 4, 10, 5, 17, 18 | 4atexlemu 39474 |
. . . . . . 7
β’ (π β π β π΄) |
24 | 2, 9, 4, 10, 5, 17, 18, 19 | 4atexlemunv 39476 |
. . . . . . 7
β’ (π β π β π) |
25 | 2 | 4atexlemutvt 39464 |
. . . . . . 7
β’ (π β (π β¨ π) = (π β¨ π)) |
26 | 5, 4 | cvlsupr6 38756 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π) = (π β¨ π))) β π β π) |
27 | 26 | necomd 2991 |
. . . . . . 7
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π) = (π β¨ π))) β π β π) |
28 | 16, 23, 20, 22, 24, 25, 27 | syl132anc 1386 |
. . . . . 6
β’ (π β π β π) |
29 | 9, 4, 5 | cvlatexch2 38746 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
30 | 16, 20, 21, 22, 28, 29 | syl131anc 1381 |
. . . . 5
β’ (π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
31 | 2, 17 | 4atexlemwb 39469 |
. . . . . . . . 9
β’ (π β π β (BaseβπΎ)) |
32 | 8, 9, 10 | latmle2 18448 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β§ π) β€ π) |
33 | 3, 7, 31, 32 | syl3anc 1369 |
. . . . . . . 8
β’ (π β ((π β¨ π) β§ π) β€ π) |
34 | 19, 33 | eqbrtrid 5177 |
. . . . . . 7
β’ (π β π β€ π) |
35 | 2, 9, 4, 10, 5, 17, 18, 19 | 4atexlemtlw 39477 |
. . . . . . 7
β’ (π β π β€ π) |
36 | 8, 5 | atbase 38698 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
37 | 20, 36 | syl 17 |
. . . . . . . 8
β’ (π β π β (BaseβπΎ)) |
38 | 8, 5 | atbase 38698 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
39 | 22, 38 | syl 17 |
. . . . . . . 8
β’ (π β π β (BaseβπΎ)) |
40 | 8, 9, 4 | latjle12 18433 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
41 | 3, 37, 39, 31, 40 | syl13anc 1370 |
. . . . . . 7
β’ (π β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
42 | 34, 35, 41 | mpbi2and 711 |
. . . . . 6
β’ (π β (π β¨ π) β€ π) |
43 | 8, 5 | atbase 38698 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
44 | 21, 43 | syl 17 |
. . . . . . 7
β’ (π β π β (BaseβπΎ)) |
45 | 2 | 4atexlemk 39457 |
. . . . . . . 8
β’ (π β πΎ β HL) |
46 | 8, 4, 5 | hlatjcl 38776 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
47 | 45, 20, 22, 46 | syl3anc 1369 |
. . . . . . 7
β’ (π β (π β¨ π) β (BaseβπΎ)) |
48 | 8, 9 | lattr 18427 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β€ (π β¨ π) β§ (π β¨ π) β€ π) β π β€ π)) |
49 | 3, 44, 47, 31, 48 | syl13anc 1370 |
. . . . . 6
β’ (π β ((π β€ (π β¨ π) β§ (π β¨ π) β€ π) β π β€ π)) |
50 | 42, 49 | mpan2d 693 |
. . . . 5
β’ (π β (π β€ (π β¨ π) β π β€ π)) |
51 | 30, 50 | syld 47 |
. . . 4
β’ (π β (π β€ (π β¨ π) β π β€ π)) |
52 | 15, 51 | mtod 197 |
. . 3
β’ (π β Β¬ π β€ (π β¨ π)) |
53 | | nbrne2 5162 |
. . 3
β’ ((πΆ β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β πΆ β π) |
54 | 13, 52, 53 | syl2anc 583 |
. 2
β’ (π β πΆ β π) |
55 | 2 | 4atexlemw 39458 |
. . . 4
β’ (π β π β π») |
56 | 45, 55 | jca 511 |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
57 | 2 | 4atexlempw 39459 |
. . 3
β’ (π β (π β π΄ β§ Β¬ π β€ π)) |
58 | 2 | 4atexlems 39462 |
. . 3
β’ (π β π β π΄) |
59 | 2, 9, 4, 10, 5, 17, 18, 19, 1 | 4atexlemc 39479 |
. . 3
β’ (π β πΆ β π΄) |
60 | 2, 9, 4, 5 | 4atexlempns 39472 |
. . 3
β’ (π β π β π) |
61 | 8, 9, 10 | latmle2 18448 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
62 | 3, 6, 7, 61 | syl3anc 1369 |
. . . 4
β’ (π β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
63 | 1, 62 | eqbrtrid 5177 |
. . 3
β’ (π β πΆ β€ (π β¨ π)) |
64 | 9, 4, 10, 5, 17, 19 | lhpat3 39456 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ πΆ β π΄) β§ (π β π β§ πΆ β€ (π β¨ π))) β (Β¬ πΆ β€ π β πΆ β π)) |
65 | 56, 57, 58, 59, 60, 63, 64 | syl222anc 1384 |
. 2
β’ (π β (Β¬ πΆ β€ π β πΆ β π)) |
66 | 54, 65 | mpbird 257 |
1
β’ (π β Β¬ πΆ β€ π) |