Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
β’
(joinβπΎ) =
(joinβπΎ) |
2 | | eqid 2737 |
. . 3
β’
(meetβπΎ) =
(meetβπΎ) |
3 | | eqid 2737 |
. . 3
β’
(ocβπΎ) =
(ocβπΎ) |
4 | | docacl.h |
. . 3
β’ π» = (LHypβπΎ) |
5 | | docacl.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
6 | | docacl.i |
. . 3
β’ πΌ = ((DIsoAβπΎ)βπ) |
7 | | docacl.n |
. . 3
β’ β₯ =
((ocAβπΎ)βπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | docavalN 39589 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) = (πΌβ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π))) |
9 | 4, 6 | diaf11N 39515 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β πΌ:dom πΌβ1-1-ontoβran
πΌ) |
10 | | f1ofun 6787 |
. . . . 5
β’ (πΌ:dom πΌβ1-1-ontoβran
πΌ β Fun πΌ) |
11 | 9, 10 | syl 17 |
. . . 4
β’ ((πΎ β HL β§ π β π») β Fun πΌ) |
12 | 11 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β Fun πΌ) |
13 | | hllat 37828 |
. . . . . 6
β’ (πΎ β HL β πΎ β Lat) |
14 | 13 | ad2antrr 725 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΎ β Lat) |
15 | | hlop 37827 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
16 | 15 | ad2antrr 725 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β πΎ β OP) |
17 | | simpl 484 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΎ β HL β§ π β π»)) |
18 | | ssrab2 4038 |
. . . . . . . . . . 11
β’ {π§ β ran πΌ β£ π β π§} β ran πΌ |
19 | 18 | a1i 11 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β π) β {π§ β ran πΌ β£ π β π§} β ran πΌ) |
20 | 4, 5, 6 | dia1elN 39520 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π») β π β ran πΌ) |
21 | 20 | anim1i 616 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β ran πΌ β§ π β π)) |
22 | | sseq2 3971 |
. . . . . . . . . . . . 13
β’ (π§ = π β (π β π§ β π β π)) |
23 | 22 | elrab 3646 |
. . . . . . . . . . . 12
β’ (π β {π§ β ran πΌ β£ π β π§} β (π β ran πΌ β§ π β π)) |
24 | 21, 23 | sylibr 233 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β {π§ β ran πΌ β£ π β π§}) |
25 | 24 | ne0d 4296 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β π) β {π§ β ran πΌ β£ π β π§} β β
) |
26 | 4, 6 | diaintclN 39524 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ ({π§ β ran πΌ β£ π β π§} β ran πΌ β§ {π§ β ran πΌ β£ π β π§} β β
)) β β© {π§
β ran πΌ β£ π β π§} β ran πΌ) |
27 | 17, 19, 25, 26 | syl12anc 836 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β π) β β© {π§ β ran πΌ β£ π β π§} β ran πΌ) |
28 | 4, 6 | diacnvclN 39517 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ β© {π§ β ran πΌ β£ π β π§} β ran πΌ) β (β‘πΌββ© {π§ β ran πΌ β£ π β π§}) β dom πΌ) |
29 | 27, 28 | syldan 592 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β (β‘πΌββ© {π§ β ran πΌ β£ π β π§}) β dom πΌ) |
30 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
31 | 30, 4, 6 | diadmclN 39503 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (β‘πΌββ© {π§ β ran πΌ β£ π β π§}) β dom πΌ) β (β‘πΌββ© {π§ β ran πΌ β£ π β π§}) β (BaseβπΎ)) |
32 | 29, 31 | syldan 592 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β (β‘πΌββ© {π§ β ran πΌ β£ π β π§}) β (BaseβπΎ)) |
33 | 30, 3 | opoccl 37659 |
. . . . . . 7
β’ ((πΎ β OP β§ (β‘πΌββ© {π§ β ran πΌ β£ π β π§}) β (BaseβπΎ)) β ((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β (BaseβπΎ)) |
34 | 16, 32, 33 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β (BaseβπΎ)) |
35 | 30, 4 | lhpbase 38464 |
. . . . . . . 8
β’ (π β π» β π β (BaseβπΎ)) |
36 | 35 | ad2antlr 726 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β π β (BaseβπΎ)) |
37 | 30, 3 | opoccl 37659 |
. . . . . . 7
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
38 | 16, 36, 37 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
39 | 30, 1 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§
((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β (BaseβπΎ) β§ ((ocβπΎ)βπ) β (BaseβπΎ)) β (((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ)) β (BaseβπΎ)) |
40 | 14, 34, 38, 39 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ)) β (BaseβπΎ)) |
41 | 30, 2 | latmcl 18330 |
. . . . 5
β’ ((πΎ β Lat β§
(((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) |
42 | 14, 40, 36, 41 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) |
43 | | eqid 2737 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
44 | 30, 43, 2 | latmle2 18355 |
. . . . 5
β’ ((πΎ β Lat β§
(((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π) |
45 | 14, 40, 36, 44 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π) |
46 | 30, 43, 4, 6 | diaeldm 39502 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β (((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π))) |
47 | 46 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β (((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π))) |
48 | 42, 45, 47 | mpbir2and 712 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ) |
49 | | fvelrn 7028 |
. . 3
β’ ((Fun
πΌ β§ ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ) β (πΌβ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π)) β ran πΌ) |
50 | 12, 48, 49 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ((((ocβπΎ)β(β‘πΌββ© {π§ β ran πΌ β£ π β π§}))(joinβπΎ)((ocβπΎ)βπ))(meetβπΎ)π)) β ran πΌ) |
51 | 8, 50 | eqeltrd 2838 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β ran πΌ) |