Step | Hyp | Ref
| Expression |
1 | | sseqin2 4176 |
. . . . 5
β’ (π β π΅ β (π΅ β© π) = π) |
2 | 1 | biimpi 215 |
. . . 4
β’ (π β π΅ β (π΅ β© π) = π) |
3 | | dfin5 3919 |
. . . 4
β’ (π΅ β© π) = {π₯ β π΅ β£ π₯ β π} |
4 | 2, 3 | eqtr3di 2788 |
. . 3
β’ (π β π΅ β π = {π₯ β π΅ β£ π₯ β π}) |
5 | 4 | fveq2d 6847 |
. 2
β’ (π β π΅ β (πΊβπ) = (πΊβ{π₯ β π΅ β£ π₯ β π})) |
6 | | glbcon.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
7 | | eqid 2733 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
8 | | glbcon.g |
. . . 4
β’ πΊ = (glbβπΎ) |
9 | | biid 261 |
. . . 4
β’
((βπ§ β
{π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦)) β (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦))) |
10 | | id 22 |
. . . 4
β’ (πΎ β HL β πΎ β HL) |
11 | | ssrab2 4038 |
. . . . 5
β’ {π₯ β π΅ β£ π₯ β π} β π΅ |
12 | 11 | a1i 11 |
. . . 4
β’ (πΎ β HL β {π₯ β π΅ β£ π₯ β π} β π΅) |
13 | 6, 7, 8, 9, 10, 12 | glbval 18263 |
. . 3
β’ (πΎ β HL β (πΊβ{π₯ β π΅ β£ π₯ β π}) = (β©π¦ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦)))) |
14 | | hlop 37870 |
. . . 4
β’ (πΎ β HL β πΎ β OP) |
15 | | hlclat 37866 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
16 | 6, 8 | clatglbcl2 18400 |
. . . . . 6
β’ ((πΎ β CLat β§ {π₯ β π΅ β£ π₯ β π} β π΅) β {π₯ β π΅ β£ π₯ β π} β dom πΊ) |
17 | 15, 12, 16 | syl2anc 585 |
. . . . 5
β’ (πΎ β HL β {π₯ β π΅ β£ π₯ β π} β dom πΊ) |
18 | 6, 7, 8, 9, 10, 17 | glbeu 18262 |
. . . 4
β’ (πΎ β HL β β!π¦ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦))) |
19 | | glbcon.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
20 | | breq1 5109 |
. . . . . . 7
β’ (π¦ = ( β₯ βπ£) β (π¦(leβπΎ)π§ β ( β₯ βπ£)(leβπΎ)π§)) |
21 | 20 | ralbidv 3171 |
. . . . . 6
β’ (π¦ = ( β₯ βπ£) β (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§)) |
22 | | breq2 5110 |
. . . . . . . 8
β’ (π¦ = ( β₯ βπ£) β (π€(leβπΎ)π¦ β π€(leβπΎ)( β₯ βπ£))) |
23 | 22 | imbi2d 341 |
. . . . . . 7
β’ (π¦ = ( β₯ βπ£) β ((βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦) β (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)))) |
24 | 23 | ralbidv 3171 |
. . . . . 6
β’ (π¦ = ( β₯ βπ£) β (βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦) β βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)))) |
25 | 21, 24 | anbi12d 632 |
. . . . 5
β’ (π¦ = ( β₯ βπ£) β ((βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦)) β (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£))))) |
26 | 6, 19, 25 | riotaocN 37717 |
. . . 4
β’ ((πΎ β OP β§ β!π¦ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦))) β (β©π¦ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦))) = ( β₯
β(β©π£
β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)))))) |
27 | 14, 18, 26 | syl2anc 585 |
. . 3
β’ (πΎ β HL β
(β©π¦ β
π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π¦(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)π¦))) = ( β₯
β(β©π£
β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)))))) |
28 | 14 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π’ β π΅) β πΎ β OP) |
29 | 6, 19 | opoccl 37702 |
. . . . . . . . . . 11
β’ ((πΎ β OP β§ π’ β π΅) β ( β₯ βπ’) β π΅) |
30 | 28, 29 | sylancom 589 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π’ β π΅) β ( β₯ βπ’) β π΅) |
31 | 14 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π£ β π΅) β§ π§ β π΅) β πΎ β OP) |
32 | 6, 19 | opoccl 37702 |
. . . . . . . . . . . 12
β’ ((πΎ β OP β§ π§ β π΅) β ( β₯ βπ§) β π΅) |
33 | 31, 32 | sylancom 589 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π§ β π΅) β ( β₯ βπ§) β π΅) |
34 | 6, 19 | opococ 37703 |
. . . . . . . . . . . . 13
β’ ((πΎ β OP β§ π§ β π΅) β ( β₯ β( β₯
βπ§)) = π§) |
35 | 31, 34 | sylancom 589 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π£ β π΅) β§ π§ β π΅) β ( β₯ β( β₯
βπ§)) = π§) |
36 | 35 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π§ β π΅) β π§ = ( β₯ β( β₯
βπ§))) |
37 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π’ = ( β₯ βπ§) β ( β₯ βπ’) = ( β₯ β( β₯
βπ§))) |
38 | 37 | rspceeqv 3596 |
. . . . . . . . . . 11
β’ ((( β₯
βπ§) β π΅ β§ π§ = ( β₯ β( β₯
βπ§))) β
βπ’ β π΅ π§ = ( β₯ βπ’)) |
39 | 33, 36, 38 | syl2anc 585 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π§ β π΅) β βπ’ β π΅ π§ = ( β₯ βπ’)) |
40 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π§ = ( β₯ βπ’) β (π§ β π β ( β₯ βπ’) β π)) |
41 | | breq2 5110 |
. . . . . . . . . . . 12
β’ (π§ = ( β₯ βπ’) β (( β₯ βπ£)(leβπΎ)π§ β ( β₯ βπ£)(leβπΎ)( β₯ βπ’))) |
42 | 40, 41 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π§ = ( β₯ βπ’) β ((π§ β π β ( β₯ βπ£)(leβπΎ)π§) β (( β₯ βπ’) β π β ( β₯ βπ£)(leβπΎ)( β₯ βπ’)))) |
43 | 42 | adantl 483 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π§ = ( β₯ βπ’)) β ((π§ β π β ( β₯ βπ£)(leβπΎ)π§) β (( β₯ βπ’) β π β ( β₯ βπ£)(leβπΎ)( β₯ βπ’)))) |
44 | 30, 39, 43 | ralxfrd 5364 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π£ β π΅) β (βπ§ β π΅ (π§ β π β ( β₯ βπ£)(leβπΎ)π§) β βπ’ β π΅ (( β₯ βπ’) β π β ( β₯ βπ£)(leβπΎ)( β₯ βπ’)))) |
45 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π£ β π΅) β§ π’ β π΅) β π’ β π΅) |
46 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π£ β π΅) β§ π’ β π΅) β π£ β π΅) |
47 | 6, 7, 19 | oplecon3b 37708 |
. . . . . . . . . . . 12
β’ ((πΎ β OP β§ π’ β π΅ β§ π£ β π΅) β (π’(leβπΎ)π£ β ( β₯ βπ£)(leβπΎ)( β₯ βπ’))) |
48 | 28, 45, 46, 47 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π’ β π΅) β (π’(leβπΎ)π£ β ( β₯ βπ£)(leβπΎ)( β₯ βπ’))) |
49 | 48 | imbi2d 341 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π’ β π΅) β ((( β₯ βπ’) β π β π’(leβπΎ)π£) β (( β₯ βπ’) β π β ( β₯ βπ£)(leβπΎ)( β₯ βπ’)))) |
50 | 49 | ralbidva 3169 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π£ β π΅) β (βπ’ β π΅ (( β₯ βπ’) β π β π’(leβπΎ)π£) β βπ’ β π΅ (( β₯ βπ’) β π β ( β₯ βπ£)(leβπΎ)( β₯ βπ’)))) |
51 | 44, 50 | bitr4d 282 |
. . . . . . . 8
β’ ((πΎ β HL β§ π£ β π΅) β (βπ§ β π΅ (π§ β π β ( β₯ βπ£)(leβπΎ)π§) β βπ’ β π΅ (( β₯ βπ’) β π β π’(leβπΎ)π£))) |
52 | | eleq1 2822 |
. . . . . . . . 9
β’ (π₯ = π§ β (π₯ β π β π§ β π)) |
53 | 52 | ralrab 3652 |
. . . . . . . 8
β’
(βπ§ β
{π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β βπ§ β π΅ (π§ β π β ( β₯ βπ£)(leβπΎ)π§)) |
54 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π₯ = π’ β ( β₯ βπ₯) = ( β₯ βπ’)) |
55 | 54 | eleq1d 2819 |
. . . . . . . . 9
β’ (π₯ = π’ β (( β₯ βπ₯) β π β ( β₯ βπ’) β π)) |
56 | 55 | ralrab 3652 |
. . . . . . . 8
β’
(βπ’ β
{π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β βπ’ β π΅ (( β₯ βπ’) β π β π’(leβπΎ)π£)) |
57 | 51, 53, 56 | 3bitr4g 314 |
. . . . . . 7
β’ ((πΎ β HL β§ π£ β π΅) β (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£)) |
58 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β πΎ β OP) |
59 | 6, 19 | opoccl 37702 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π‘ β π΅) β ( β₯ βπ‘) β π΅) |
60 | 58, 59 | sylancom 589 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β ( β₯ βπ‘) β π΅) |
61 | 14 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π€ β π΅) β πΎ β OP) |
62 | 6, 19 | opoccl 37702 |
. . . . . . . . . . 11
β’ ((πΎ β OP β§ π€ β π΅) β ( β₯ βπ€) β π΅) |
63 | 61, 62 | sylancom 589 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π€ β π΅) β ( β₯ βπ€) β π΅) |
64 | 6, 19 | opococ 37703 |
. . . . . . . . . . . 12
β’ ((πΎ β OP β§ π€ β π΅) β ( β₯ β( β₯
βπ€)) = π€) |
65 | 61, 64 | sylancom 589 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π€ β π΅) β ( β₯ β( β₯
βπ€)) = π€) |
66 | 65 | eqcomd 2739 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π€ β π΅) β π€ = ( β₯ β( β₯
βπ€))) |
67 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π‘ = ( β₯ βπ€) β ( β₯ βπ‘) = ( β₯ β( β₯
βπ€))) |
68 | 67 | rspceeqv 3596 |
. . . . . . . . . 10
β’ ((( β₯
βπ€) β π΅ β§ π€ = ( β₯ β( β₯
βπ€))) β
βπ‘ β π΅ π€ = ( β₯ βπ‘)) |
69 | 63, 66, 68 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π£ β π΅) β§ π€ β π΅) β βπ‘ β π΅ π€ = ( β₯ βπ‘)) |
70 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π€ = ( β₯ βπ‘) β (π€(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)π§)) |
71 | 70 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π€ = ( β₯ βπ‘) β (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§)) |
72 | | breq1 5109 |
. . . . . . . . . . 11
β’ (π€ = ( β₯ βπ‘) β (π€(leβπΎ)( β₯ βπ£) β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£))) |
73 | 71, 72 | imbi12d 345 |
. . . . . . . . . 10
β’ (π€ = ( β₯ βπ‘) β ((βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)) β (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£)))) |
74 | 73 | adantl 483 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π£ β π΅) β§ π€ = ( β₯ βπ‘)) β ((βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)) β (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£)))) |
75 | 60, 69, 74 | ralxfrd 5364 |
. . . . . . . 8
β’ ((πΎ β HL β§ π£ β π΅) β (βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)) β βπ‘ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£)))) |
76 | 14 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π’ β π΅) β πΎ β OP) |
77 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π’ β π΅) β π’ β π΅) |
78 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π’ β π΅) β π‘ β π΅) |
79 | 6, 7, 19 | oplecon3b 37708 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β OP β§ π’ β π΅ β§ π‘ β π΅) β (π’(leβπΎ)π‘ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’))) |
80 | 76, 77, 78, 79 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π’ β π΅) β (π’(leβπΎ)π‘ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’))) |
81 | 80 | imbi2d 341 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π’ β π΅) β ((( β₯ βπ’) β π β π’(leβπΎ)π‘) β (( β₯ βπ’) β π β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’)))) |
82 | 81 | ralbidva 3169 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β (βπ’ β π΅ (( β₯ βπ’) β π β π’(leβπΎ)π‘) β βπ’ β π΅ (( β₯ βπ’) β π β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’)))) |
83 | 76, 29 | sylancom 589 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π’ β π΅) β ( β₯ βπ’) β π΅) |
84 | 14 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π§ β π΅) β πΎ β OP) |
85 | 84, 32 | sylancom 589 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π§ β π΅) β ( β₯ βπ§) β π΅) |
86 | 84, 34 | sylancom 589 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π§ β π΅) β ( β₯ β( β₯
βπ§)) = π§) |
87 | 86 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π§ β π΅) β π§ = ( β₯ β( β₯
βπ§))) |
88 | 85, 87, 38 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π§ β π΅) β βπ’ β π΅ π§ = ( β₯ βπ’)) |
89 | | breq2 5110 |
. . . . . . . . . . . . . . 15
β’ (π§ = ( β₯ βπ’) β (( β₯ βπ‘)(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’))) |
90 | 40, 89 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π§ = ( β₯ βπ’) β ((π§ β π β ( β₯ βπ‘)(leβπΎ)π§) β (( β₯ βπ’) β π β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’)))) |
91 | 90 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β§ π§ = ( β₯ βπ’)) β ((π§ β π β ( β₯ βπ‘)(leβπΎ)π§) β (( β₯ βπ’) β π β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’)))) |
92 | 83, 88, 91 | ralxfrd 5364 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β (βπ§ β π΅ (π§ β π β ( β₯ βπ‘)(leβπΎ)π§) β βπ’ β π΅ (( β₯ βπ’) β π β ( β₯ βπ‘)(leβπΎ)( β₯ βπ’)))) |
93 | 82, 92 | bitr4d 282 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β (βπ’ β π΅ (( β₯ βπ’) β π β π’(leβπΎ)π‘) β βπ§ β π΅ (π§ β π β ( β₯ βπ‘)(leβπΎ)π§))) |
94 | 55 | ralrab 3652 |
. . . . . . . . . . 11
β’
(βπ’ β
{π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β βπ’ β π΅ (( β₯ βπ’) β π β π’(leβπΎ)π‘)) |
95 | 52 | ralrab 3652 |
. . . . . . . . . . 11
β’
(βπ§ β
{π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§ β βπ§ β π΅ (π§ β π β ( β₯ βπ‘)(leβπΎ)π§)) |
96 | 93, 94, 95 | 3bitr4g 314 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§)) |
97 | | simplr 768 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β π£ β π΅) |
98 | | simpr 486 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β π‘ β π΅) |
99 | 6, 7, 19 | oplecon3b 37708 |
. . . . . . . . . . 11
β’ ((πΎ β OP β§ π£ β π΅ β§ π‘ β π΅) β (π£(leβπΎ)π‘ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£))) |
100 | 58, 97, 98, 99 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β (π£(leβπΎ)π‘ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£))) |
101 | 96, 100 | imbi12d 345 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π£ β π΅) β§ π‘ β π΅) β ((βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘) β (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£)))) |
102 | 101 | ralbidva 3169 |
. . . . . . . 8
β’ ((πΎ β HL β§ π£ β π΅) β (βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘) β βπ‘ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ‘)(leβπΎ)π§ β ( β₯ βπ‘)(leβπΎ)( β₯ βπ£)))) |
103 | 75, 102 | bitr4d 282 |
. . . . . . 7
β’ ((πΎ β HL β§ π£ β π΅) β (βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)) β βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘))) |
104 | 57, 103 | anbi12d 632 |
. . . . . 6
β’ ((πΎ β HL β§ π£ β π΅) β ((βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£))) β (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β§ βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘)))) |
105 | 104 | riotabidva 7334 |
. . . . 5
β’ (πΎ β HL β
(β©π£ β
π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)))) = (β©π£ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β§ βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘)))) |
106 | | ssrab2 4038 |
. . . . . 6
β’ {π₯ β π΅ β£ ( β₯ βπ₯) β π} β π΅ |
107 | | glbcon.u |
. . . . . . 7
β’ π = (lubβπΎ) |
108 | | biid 261 |
. . . . . . 7
β’
((βπ’ β
{π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β§ βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘)) β (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β§ βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘))) |
109 | | simpl 484 |
. . . . . . 7
β’ ((πΎ β HL β§ {π₯ β π΅ β£ ( β₯ βπ₯) β π} β π΅) β πΎ β HL) |
110 | | simpr 486 |
. . . . . . 7
β’ ((πΎ β HL β§ {π₯ β π΅ β£ ( β₯ βπ₯) β π} β π΅) β {π₯ β π΅ β£ ( β₯ βπ₯) β π} β π΅) |
111 | 6, 7, 107, 108, 109, 110 | lubval 18250 |
. . . . . 6
β’ ((πΎ β HL β§ {π₯ β π΅ β£ ( β₯ βπ₯) β π} β π΅) β (πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}) = (β©π£ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β§ βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘)))) |
112 | 106, 111 | mpan2 690 |
. . . . 5
β’ (πΎ β HL β (πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}) = (β©π£ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π£ β§ βπ‘ β π΅ (βπ’ β {π₯ β π΅ β£ ( β₯ βπ₯) β π}π’(leβπΎ)π‘ β π£(leβπΎ)π‘)))) |
113 | 105, 112 | eqtr4d 2776 |
. . . 4
β’ (πΎ β HL β
(β©π£ β
π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£)))) = (πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π})) |
114 | 113 | fveq2d 6847 |
. . 3
β’ (πΎ β HL β ( β₯
β(β©π£
β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π} ( β₯ βπ£)(leβπΎ)π§ β§ βπ€ β π΅ (βπ§ β {π₯ β π΅ β£ π₯ β π}π€(leβπΎ)π§ β π€(leβπΎ)( β₯ βπ£))))) = ( β₯ β(πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}))) |
115 | 13, 27, 114 | 3eqtrd 2777 |
. 2
β’ (πΎ β HL β (πΊβ{π₯ β π΅ β£ π₯ β π}) = ( β₯ β(πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}))) |
116 | 5, 115 | sylan9eqr 2795 |
1
β’ ((πΎ β HL β§ π β π΅) β (πΊβπ) = ( β₯ β(πβ{π₯ β π΅ β£ ( β₯ βπ₯) β π}))) |