Step | Hyp | Ref
| Expression |
1 | | lubfval.k |
. 2
β’ (π β πΎ β π) |
2 | | elex 3492 |
. 2
β’ (πΎ β π β πΎ β V) |
3 | | fveq2 6891 |
. . . . . . . 8
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
4 | | lubfval.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
5 | 3, 4 | eqtr4di 2790 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = π΅) |
6 | 5 | pweqd 4619 |
. . . . . 6
β’ (π = πΎ β π« (Baseβπ) = π« π΅) |
7 | | fveq2 6891 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
8 | | lubfval.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
9 | 7, 8 | eqtr4di 2790 |
. . . . . . . . . 10
β’ (π = πΎ β (leβπ) = β€ ) |
10 | 9 | breqd 5159 |
. . . . . . . . 9
β’ (π = πΎ β (π¦(leβπ)π₯ β π¦ β€ π₯)) |
11 | 10 | ralbidv 3177 |
. . . . . . . 8
β’ (π = πΎ β (βπ¦ β π π¦(leβπ)π₯ β βπ¦ β π π¦ β€ π₯)) |
12 | 9 | breqd 5159 |
. . . . . . . . . . 11
β’ (π = πΎ β (π¦(leβπ)π§ β π¦ β€ π§)) |
13 | 12 | ralbidv 3177 |
. . . . . . . . . 10
β’ (π = πΎ β (βπ¦ β π π¦(leβπ)π§ β βπ¦ β π π¦ β€ π§)) |
14 | 9 | breqd 5159 |
. . . . . . . . . 10
β’ (π = πΎ β (π₯(leβπ)π§ β π₯ β€ π§)) |
15 | 13, 14 | imbi12d 344 |
. . . . . . . . 9
β’ (π = πΎ β ((βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§) β (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
16 | 5, 15 | raleqbidv 3342 |
. . . . . . . 8
β’ (π = πΎ β (βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
17 | 11, 16 | anbi12d 631 |
. . . . . . 7
β’ (π = πΎ β ((βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)) β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
18 | 5, 17 | riotaeqbidv 7367 |
. . . . . 6
β’ (π = πΎ β (β©π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§))) = (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
19 | 6, 18 | mpteq12dv 5239 |
. . . . 5
β’ (π = πΎ β (π β π« (Baseβπ) β¦ (β©π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)))) = (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))))) |
20 | 17 | reubidv 3394 |
. . . . . . 7
β’ (π = πΎ β (β!π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)) β β!π₯ β (Baseβπ)(βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
21 | | reueq1 3415 |
. . . . . . . 8
β’
((Baseβπ) =
π΅ β (β!π₯ β (Baseβπ)(βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
22 | 5, 21 | syl 17 |
. . . . . . 7
β’ (π = πΎ β (β!π₯ β (Baseβπ)(βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
23 | 20, 22 | bitrd 278 |
. . . . . 6
β’ (π = πΎ β (β!π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)) β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
24 | 23 | abbidv 2801 |
. . . . 5
β’ (π = πΎ β {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§))} = {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))}) |
25 | 19, 24 | reseq12d 5982 |
. . . 4
β’ (π = πΎ β ((π β π« (Baseβπ) β¦ (β©π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)))) βΎ {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§))}) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))})) |
26 | | df-lub 18298 |
. . . 4
β’ lub =
(π β V β¦ ((π β π«
(Baseβπ) β¦
(β©π₯ β
(Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§)))) βΎ {π β£ β!π₯ β (Baseβπ)(βπ¦ β π π¦(leβπ)π₯ β§ βπ§ β (Baseβπ)(βπ¦ β π π¦(leβπ)π§ β π₯(leβπ)π§))})) |
27 | 4 | fvexi 6905 |
. . . . . . 7
β’ π΅ β V |
28 | 27 | pwex 5378 |
. . . . . 6
β’ π«
π΅ β V |
29 | 28 | mptex 7224 |
. . . . 5
β’ (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) β V |
30 | 29 | resex 6029 |
. . . 4
β’ ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))}) β V |
31 | 25, 26, 30 | fvmpt 6998 |
. . 3
β’ (πΎ β V β
(lubβπΎ) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))})) |
32 | | lubfval.u |
. . 3
β’ π = (lubβπΎ) |
33 | | lubfval.p |
. . . . . . 7
β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
34 | 33 | a1i 11 |
. . . . . 6
β’ (π₯ β π΅ β (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
35 | 34 | riotabiia 7385 |
. . . . 5
β’
(β©π₯
β π΅ π) = (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
36 | 35 | mpteq2i 5253 |
. . . 4
β’ (π β π« π΅ β¦ (β©π₯ β π΅ π)) = (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
37 | 33 | reubii 3385 |
. . . . 5
β’
(β!π₯ β
π΅ π β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
38 | 37 | abbii 2802 |
. . . 4
β’ {π β£ β!π₯ β π΅ π} = {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))} |
39 | 36, 38 | reseq12i 5979 |
. . 3
β’ ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π}) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))}) |
40 | 31, 32, 39 | 3eqtr4g 2797 |
. 2
β’ (πΎ β V β π = ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π})) |
41 | 1, 2, 40 | 3syl 18 |
1
β’ (π β π = ((π β π« π΅ β¦ (β©π₯ β π΅ π)) βΎ {π β£ β!π₯ β π΅ π})) |