Step | Hyp | Ref
| Expression |
1 | | glbfval.k |
. 2
β’ (π β πΎ β π) |
2 | | elex 3485 |
. 2
β’ (πΎ β π β πΎ β V) |
3 | | fveq2 6882 |
. . . . . . . 8
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | glbfval.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2782 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | 5 | pweqd 4612 |
. . . . . 6
β’ (π = πΎ β π« (Baseβπ) = π« π΅) |
7 | | fveq2 6882 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
8 | | glbfval.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
9 | 7, 8 | eqtr4di 2782 |
. . . . . . . . . 10
β’ (π = πΎ β (leβπ) = β€ ) |
10 | 9 | breqd 5150 |
. . . . . . . . 9
β’ (π = πΎ β (π₯(leβπ)π¦ β π₯ β€ π¦)) |
11 | 10 | ralbidv 3169 |
. . . . . . . 8
β’ (π = πΎ β (βπ¦ β π π₯(leβπ)π¦ β βπ¦ β π π₯ β€ π¦)) |
12 | 9 | breqd 5150 |
. . . . . . . . . . 11
β’ (π = πΎ β (π§(leβπ)π¦ β π§ β€ π¦)) |
13 | 12 | ralbidv 3169 |
. . . . . . . . . 10
β’ (π = πΎ β (βπ¦ β π π§(leβπ)π¦ β βπ¦ β π π§ β€ π¦)) |
14 | 9 | breqd 5150 |
. . . . . . . . . 10
β’ (π = πΎ β (π§(leβπ)π₯ β π§ β€ π₯)) |
15 | 13, 14 | imbi12d 344 |
. . . . . . . . 9
β’ (π = πΎ β ((βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯) β (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
16 | 5, 15 | raleqbidv 3334 |
. . . . . . . 8
β’ (π = πΎ β (βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯) β βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
17 | 11, 16 | anbi12d 630 |
. . . . . . 7
β’ (π = πΎ β ((βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)) β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
18 | 5, 17 | riotaeqbidv 7361 |
. . . . . 6
β’ (π = πΎ β (β©π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯))) = (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
19 | 6, 18 | mpteq12dv 5230 |
. . . . 5
β’ (π = πΎ β (π β π« (Baseβπ) β¦ (β©π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)))) = (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))))) |
20 | 17 | reubidv 3386 |
. . . . . . 7
β’ (π = πΎ β (β!π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)) β β!π₯ β (Baseβπ)(βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
21 | | reueq1 3407 |
. . . . . . . 8
β’
((Baseβπ) =
π΅ β (β!π₯ β (Baseβπ)(βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
22 | 5, 21 | syl 17 |
. . . . . . 7
β’ (π = πΎ β (β!π₯ β (Baseβπ)(βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
23 | 20, 22 | bitrd 279 |
. . . . . 6
β’ (π = πΎ β (β!π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)) β β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
24 | 23 | abbidv 2793 |
. . . . 5
β’ (π = πΎ β {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯))} = {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))}) |
25 | 19, 24 | reseq12d 5973 |
. . . 4
β’ (π = πΎ β ((π β π« (Baseβπ) β¦ (β©π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)))) βΎ {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯))}) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))})) |
26 | | df-glb 18308 |
. . . 4
β’ glb =
(π β V β¦ ((π β π«
(Baseβπ) β¦
(β©π₯ β
(Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯)))) βΎ {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π₯(leβπ)π¦ β§ βπ§ β (Baseβπ)(βπ¦ β π π§(leβπ)π¦ β π§(leβπ)π₯))})) |
27 | 4 | fvexi 6896 |
. . . . . . 7
β’ π΅ β V |
28 | 27 | pwex 5369 |
. . . . . 6
β’ π«
π΅ β V |
29 | 28 | mptex 7217 |
. . . . 5
β’ (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) β V |
30 | 29 | resex 6020 |
. . . 4
β’ ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))}) β V |
31 | 25, 26, 30 | fvmpt 6989 |
. . 3
β’ (πΎ β V β
(glbβπΎ) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))})) |
32 | | glbfval.g |
. . 3
β’ πΊ = (glbβπΎ) |
33 | | glbfval.p |
. . . . . . 7
β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
34 | 33 | a1i 11 |
. . . . . 6
β’ (π₯ β π΅ β (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
35 | 34 | riotabiia 7379 |
. . . . 5
β’
(β©π₯
β π΅ π) = (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
36 | 35 | mpteq2i 5244 |
. . . 4
β’ (π β π« π΅ β¦ (β©π₯ β π΅ π)) = (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
37 | 33 | reubii 3377 |
. . . . 5
β’
(β!π₯ β
π΅ π β β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
38 | 37 | abbii 2794 |
. . . 4
β’ {π β£ β!π₯ β π΅ π} = {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))} |
39 | 36, 38 | reseq12i 5970 |
. . 3
β’ ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π}) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))}) |
40 | 31, 32, 39 | 3eqtr4g 2789 |
. 2
β’ (πΎ β V β πΊ = ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π})) |
41 | 1, 2, 40 | 3syl 18 |
1
β’ (π β πΊ = ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π})) |