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