Step | Hyp | Ref
| Expression |
1 | | riotaex 7317 |
. . . . 5
β’
(β©π
β π (πβπ) = π) β V |
2 | | cdlemm10.g |
. . . . 5
β’ πΊ = (π β πΆ β¦ (β©π β π (πβπ) = π)) |
3 | 1, 2 | fnmpti 6644 |
. . . 4
β’ πΊ Fn πΆ |
4 | | fvelrnb 6903 |
. . . 4
β’ (πΊ Fn πΆ β (π β ran πΊ β βπ β πΆ (πΊβπ ) = π)) |
5 | 3, 4 | ax-mp 5 |
. . 3
β’ (π β ran πΊ β βπ β πΆ (πΊβπ ) = π) |
6 | | eqeq2 2748 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) = π β (πβπ) = π )) |
7 | 6 | riotabidv 7315 |
. . . . . . . . . . 11
β’ (π = π β (β©π β π (πβπ) = π) = (β©π β π (πβπ) = π )) |
8 | | riotaex 7317 |
. . . . . . . . . . 11
β’
(β©π
β π (πβπ) = π ) β V |
9 | 7, 2, 8 | fvmpt 6948 |
. . . . . . . . . 10
β’ (π β πΆ β (πΊβπ ) = (β©π β π (πβπ) = π )) |
10 | | cdlemm10.f |
. . . . . . . . . 10
β’ πΉ = (β©π β π (πβπ) = π ) |
11 | 9, 10 | eqtr4di 2794 |
. . . . . . . . 9
β’ (π β πΆ β (πΊβπ ) = πΉ) |
12 | 11 | adantl 482 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ π β πΆ) β (πΊβπ ) = πΉ) |
13 | 12 | eqeq1d 2738 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ π β πΆ) β ((πΊβπ ) = π β πΉ = π)) |
14 | 13 | rexbidva 3173 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (βπ β πΆ (πΊβπ ) = π β βπ β πΆ πΉ = π)) |
15 | | simpl1 1191 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (πΎ β HL β§ π β π»)) |
16 | | simprl 769 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β π β π) |
17 | | simpl2l 1226 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β π β π΄) |
18 | | cdlemm10.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
19 | | cdlemm10.a |
. . . . . . . . . . . 12
β’ π΄ = (AtomsβπΎ) |
20 | | cdlemm10.h |
. . . . . . . . . . . 12
β’ π» = (LHypβπΎ) |
21 | | cdlemm10.t |
. . . . . . . . . . . 12
β’ π = ((LTrnβπΎ)βπ) |
22 | 18, 19, 20, 21 | ltrnat 38603 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π΄) β (πβπ) β π΄) |
23 | 15, 16, 17, 22 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (πβπ) β π΄) |
24 | | eqid 2736 |
. . . . . . . . . . . 12
β’
(BaseβπΎ) =
(BaseβπΎ) |
25 | | simpl1l 1224 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β πΎ β HL) |
26 | 25 | hllatd 37826 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β πΎ β Lat) |
27 | 24, 19 | atbase 37751 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π β (BaseβπΎ)) |
28 | 17, 27 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β π β (BaseβπΎ)) |
29 | 24, 20, 21 | ltrncl 38588 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (BaseβπΎ)) β (πβπ) β (BaseβπΎ)) |
30 | 15, 16, 28, 29 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (πβπ) β (BaseβπΎ)) |
31 | | cdlemm10.j |
. . . . . . . . . . . . . 14
β’ β¨ =
(joinβπΎ) |
32 | 24, 31 | latjcl 18328 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (πβπ) β (BaseβπΎ)) β (π β¨ (πβπ)) β (BaseβπΎ)) |
33 | 26, 28, 30, 32 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π β¨ (πβπ)) β (BaseβπΎ)) |
34 | | simpl3l 1228 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β π β π΄) |
35 | 24, 31, 19 | hlatjcl 37829 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
36 | 25, 17, 34, 35 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π β¨ π) β (BaseβπΎ)) |
37 | 24, 18, 31 | latlej2 18338 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (πβπ) β (BaseβπΎ)) β (πβπ) β€ (π β¨ (πβπ))) |
38 | 26, 28, 30, 37 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (πβπ) β€ (π β¨ (πβπ))) |
39 | | simpl2 1192 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π β π΄ β§ Β¬ π β€ π)) |
40 | | cdlemm10.r |
. . . . . . . . . . . . . . 15
β’ π
= ((trLβπΎ)βπ) |
41 | 18, 31, 19, 20, 21, 40 | trljat1 38629 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπ)) = (π β¨ (πβπ))) |
42 | 15, 16, 39, 41 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π β¨ (π
βπ)) = (π β¨ (πβπ))) |
43 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π
βπ) β€ π) |
44 | 24, 20, 21, 40 | trlcl 38627 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π
βπ) β (BaseβπΎ)) |
45 | 15, 16, 44 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π
βπ) β (BaseβπΎ)) |
46 | 24, 19 | atbase 37751 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β π β (BaseβπΎ)) |
47 | 34, 46 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β π β (BaseβπΎ)) |
48 | 24, 18, 31 | latjlej2 18343 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Lat β§ ((π
βπ) β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π
βπ) β€ π β (π β¨ (π
βπ)) β€ (π β¨ π))) |
49 | 26, 45, 47, 28, 48 | syl13anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β ((π
βπ) β€ π β (π β¨ (π
βπ)) β€ (π β¨ π))) |
50 | 43, 49 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π β¨ (π
βπ)) β€ (π β¨ π)) |
51 | 42, 50 | eqbrtrrd 5129 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (π β¨ (πβπ)) β€ (π β¨ π)) |
52 | 24, 18, 26, 30, 33, 36, 38, 51 | lattrd 18335 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (πβπ) β€ (π β¨ π)) |
53 | 18, 19, 20, 21 | ltrnel 38602 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) |
54 | 53 | simprd 496 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β Β¬ (πβπ) β€ π) |
55 | 15, 16, 39, 54 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β Β¬ (πβπ) β€ π) |
56 | 52, 55 | jca 512 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β ((πβπ) β€ (π β¨ π) β§ Β¬ (πβπ) β€ π)) |
57 | | breq1 5108 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (π β€ (π β¨ π) β (πβπ) β€ (π β¨ π))) |
58 | | breq1 5108 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β (π β€ π β (πβπ) β€ π)) |
59 | 58 | notbid 317 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (Β¬ π β€ π β Β¬ (πβπ) β€ π)) |
60 | 57, 59 | anbi12d 631 |
. . . . . . . . . . 11
β’ (π = (πβπ) β ((π β€ (π β¨ π) β§ Β¬ π β€ π) β ((πβπ) β€ (π β¨ π) β§ Β¬ (πβπ) β€ π))) |
61 | | cdlemm10.c |
. . . . . . . . . . 11
β’ πΆ = {π β π΄ β£ (π β€ (π β¨ π) β§ Β¬ π β€ π)} |
62 | 60, 61 | elrab2 3648 |
. . . . . . . . . 10
β’ ((πβπ) β πΆ β ((πβπ) β π΄ β§ ((πβπ) β€ (π β¨ π) β§ Β¬ (πβπ) β€ π))) |
63 | 23, 56, 62 | sylanbrc 583 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (πβπ) β πΆ) |
64 | 18, 19, 20, 21 | cdlemeiota 39048 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β π = (β©π β π (πβπ) = (πβπ))) |
65 | 15, 39, 16, 64 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β π = (β©π β π (πβπ) = (πβπ))) |
66 | 65 | eqcomd 2742 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β (β©π β π (πβπ) = (πβπ)) = π) |
67 | | eqeq2 2748 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β ((πβπ) = π β (πβπ) = (πβπ))) |
68 | 67 | riotabidv 7315 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (β©π β π (πβπ) = π ) = (β©π β π (πβπ) = (πβπ))) |
69 | 10, 68 | eqtrid 2788 |
. . . . . . . . . . 11
β’ (π = (πβπ) β πΉ = (β©π β π (πβπ) = (πβπ))) |
70 | 69 | eqeq1d 2738 |
. . . . . . . . . 10
β’ (π = (πβπ) β (πΉ = π β (β©π β π (πβπ) = (πβπ)) = π)) |
71 | 70 | rspcev 3581 |
. . . . . . . . 9
β’ (((πβπ) β πΆ β§ (β©π β π (πβπ) = (πβπ)) = π) β βπ β πΆ πΉ = π) |
72 | 63, 66, 71 | syl2anc 584 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ (π
βπ) β€ π)) β βπ β πΆ πΉ = π) |
73 | 72 | ex 413 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β π β§ (π
βπ) β€ π) β βπ β πΆ πΉ = π)) |
74 | | breq1 5108 |
. . . . . . . . . . . . 13
β’ (π = π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
75 | | breq1 5108 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β€ π β π β€ π)) |
76 | 75 | notbid 317 |
. . . . . . . . . . . . 13
β’ (π = π β (Β¬ π β€ π β Β¬ π β€ π)) |
77 | 74, 76 | anbi12d 631 |
. . . . . . . . . . . 12
β’ (π = π β ((π β€ (π β¨ π) β§ Β¬ π β€ π) β (π β€ (π β¨ π) β§ Β¬ π β€ π))) |
78 | 77, 61 | elrab2 3648 |
. . . . . . . . . . 11
β’ (π β πΆ β (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) |
79 | | simpl1 1191 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β (πΎ β HL β§ π β π»)) |
80 | | simpl2l 1226 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β π΄) |
81 | | simpl2r 1227 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β Β¬ π β€ π) |
82 | | simprl 769 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β π΄) |
83 | | simprrr 780 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β Β¬ π β€ π) |
84 | 18, 19, 20, 21, 10 | ltrniotacl 39042 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
85 | 18, 19, 20, 21, 10 | ltrniotaval 39044 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) = π ) |
86 | 84, 85 | jca 512 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ β π β§ (πΉβπ) = π )) |
87 | 79, 80, 81, 82, 83, 86 | syl122anc 1379 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β (πΉ β π β§ (πΉβπ) = π )) |
88 | | simp3l 1201 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β πΉ β π) |
89 | | simp11 1203 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (πΎ β HL β§ π β π»)) |
90 | | simp12 1204 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (π β π΄ β§ Β¬ π β€ π)) |
91 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
β’
(meetβπΎ) =
(meetβπΎ) |
92 | 18, 31, 91, 19, 20, 21, 40 | trlval2 38626 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = ((π β¨ (πΉβπ))(meetβπΎ)π)) |
93 | 89, 88, 90, 92 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (π
βπΉ) = ((π β¨ (πΉβπ))(meetβπΎ)π)) |
94 | | simp3r 1202 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (πΉβπ) = π ) |
95 | 94 | oveq2d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (π β¨ (πΉβπ)) = (π β¨ π )) |
96 | 95 | oveq1d 7372 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β ((π β¨ (πΉβπ))(meetβπΎ)π) = ((π β¨ π )(meetβπΎ)π)) |
97 | 93, 96 | eqtrd 2776 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (π
βπΉ) = ((π β¨ π )(meetβπΎ)π)) |
98 | | simpl1l 1224 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β πΎ β HL) |
99 | | simpl3l 1228 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β π΄) |
100 | 18, 31, 19 | hlatlej1 37837 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
101 | 98, 80, 99, 100 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β€ (π β¨ π)) |
102 | | simprrl 779 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β€ (π β¨ π)) |
103 | 98 | hllatd 37826 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β πΎ β Lat) |
104 | 80, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β (BaseβπΎ)) |
105 | 24, 19 | atbase 37751 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΄ β π β (BaseβπΎ)) |
106 | 105 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β (BaseβπΎ)) |
107 | 98, 80, 99, 35 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β (π β¨ π) β (BaseβπΎ)) |
108 | 24, 18, 31 | latjle12 18339 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π ) β€ (π β¨ π))) |
109 | 103, 104,
106, 107, 108 | syl13anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β (π β¨ π ) β€ (π β¨ π))) |
110 | 101, 102,
109 | mpbi2and 710 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β (π β¨ π ) β€ (π β¨ π)) |
111 | 24, 31, 19 | hlatjcl 37829 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π ) β (BaseβπΎ)) |
112 | 98, 80, 82, 111 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β (π β¨ π ) β (BaseβπΎ)) |
113 | | simpl1r 1225 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β π») |
114 | 24, 20 | lhpbase 38461 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π» β π β (BaseβπΎ)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β π β (BaseβπΎ)) |
116 | 24, 18, 91 | latmlem1 18358 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Lat β§ ((π β¨ π ) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β¨ π ) β€ (π β¨ π) β ((π β¨ π )(meetβπΎ)π) β€ ((π β¨ π)(meetβπΎ)π))) |
117 | 103, 112,
107, 115, 116 | syl13anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β ((π β¨ π ) β€ (π β¨ π) β ((π β¨ π )(meetβπΎ)π) β€ ((π β¨ π)(meetβπΎ)π))) |
118 | 110, 117 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β ((π β¨ π )(meetβπΎ)π) β€ ((π β¨ π)(meetβπΎ)π)) |
119 | 18, 31, 91, 19, 20 | lhpat4N 38507 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β¨ π)(meetβπΎ)π) = π) |
120 | 119 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β ((π β¨ π)(meetβπΎ)π) = π) |
121 | 118, 120 | breqtrd 5131 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β ((π β¨ π )(meetβπΎ)π) β€ π) |
122 | 121 | 3adant3 1132 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β ((π β¨ π )(meetβπΎ)π) β€ π) |
123 | 97, 122 | eqbrtrd 5127 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (π
βπΉ) β€ π) |
124 | 88, 123 | jca 512 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π )) β (πΉ β π β§ (π
βπΉ) β€ π)) |
125 | 87, 124 | mpd3an3 1462 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π΄ β§ (π β€ (π β¨ π) β§ Β¬ π β€ π))) β (πΉ β π β§ (π
βπΉ) β€ π)) |
126 | 78, 125 | sylan2b 594 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ π β πΆ) β (πΉ β π β§ (π
βπΉ) β€ π)) |
127 | 126 | ex 413 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β πΆ β (πΉ β π β§ (π
βπΉ) β€ π))) |
128 | | eleq1 2825 |
. . . . . . . . . . 11
β’ (πΉ = π β (πΉ β π β π β π)) |
129 | | fveq2 6842 |
. . . . . . . . . . . 12
β’ (πΉ = π β (π
βπΉ) = (π
βπ)) |
130 | 129 | breq1d 5115 |
. . . . . . . . . . 11
β’ (πΉ = π β ((π
βπΉ) β€ π β (π
βπ) β€ π)) |
131 | 128, 130 | anbi12d 631 |
. . . . . . . . . 10
β’ (πΉ = π β ((πΉ β π β§ (π
βπΉ) β€ π) β (π β π β§ (π
βπ) β€ π))) |
132 | 131 | biimpcd 248 |
. . . . . . . . 9
β’ ((πΉ β π β§ (π
βπΉ) β€ π) β (πΉ = π β (π β π β§ (π
βπ) β€ π))) |
133 | 127, 132 | syl6 35 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β πΆ β (πΉ = π β (π β π β§ (π
βπ) β€ π)))) |
134 | 133 | rexlimdv 3150 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (βπ β πΆ πΉ = π β (π β π β§ (π
βπ) β€ π))) |
135 | 73, 134 | impbid 211 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β π β§ (π
βπ) β€ π) β βπ β πΆ πΉ = π)) |
136 | 14, 135 | bitr4d 281 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (βπ β πΆ (πΊβπ ) = π β (π β π β§ (π
βπ) β€ π))) |
137 | | fveq2 6842 |
. . . . . . 7
β’ (π = π β (π
βπ) = (π
βπ)) |
138 | 137 | breq1d 5115 |
. . . . . 6
β’ (π = π β ((π
βπ) β€ π β (π
βπ) β€ π)) |
139 | 138 | elrab 3645 |
. . . . 5
β’ (π β {π β π β£ (π
βπ) β€ π} β (π β π β§ (π
βπ) β€ π)) |
140 | 136, 139 | bitr4di 288 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (βπ β πΆ (πΊβπ ) = π β π β {π β π β£ (π
βπ) β€ π})) |
141 | | simp1l 1197 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β πΎ β HL) |
142 | | simp1r 1198 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β π») |
143 | | simp3l 1201 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β π΄) |
144 | 143, 46 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β (BaseβπΎ)) |
145 | | simp3r 1202 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β π β€ π) |
146 | | cdlemm10.i |
. . . . . . 7
β’ πΌ = ((DIsoAβπΎ)βπ) |
147 | 24, 18, 20, 21, 40, 146 | diaval 39495 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β (BaseβπΎ) β§ π β€ π)) β (πΌβπ) = {π β π β£ (π
βπ) β€ π}) |
148 | 141, 142,
144, 145, 147 | syl22anc 837 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (πΌβπ) = {π β π β£ (π
βπ) β€ π}) |
149 | 148 | eleq2d 2823 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β (πΌβπ) β π β {π β π β£ (π
βπ) β€ π})) |
150 | 140, 149 | bitr4d 281 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (βπ β πΆ (πΊβπ ) = π β π β (πΌβπ))) |
151 | 5, 150 | bitrid 282 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β ran πΊ β π β (πΌβπ))) |
152 | 151 | eqrdv 2734 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β ran πΊ = (πΌβπ)) |