Step | Hyp | Ref
| Expression |
1 | | glbval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | glbval.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | glbval.g |
. . . . 5
β’ πΊ = (glbβπΎ) |
4 | | biid 262 |
. . . . 5
β’
((βπ¦ β
π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
5 | | glbva.k |
. . . . . 6
β’ (π β πΎ β π) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π β dom πΊ) β πΎ β π) |
7 | 1, 2, 3, 4, 6 | glbfval 18122 |
. . . 4
β’ ((π β§ π β dom πΊ) β πΊ = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))})) |
8 | 7 | fveq1d 6802 |
. . 3
β’ ((π β§ π β dom πΊ) β (πΊβπ) = (((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))})βπ)) |
9 | | simpr 486 |
. . . . 5
β’ ((π β§ π β dom πΊ) β π β dom πΊ) |
10 | | glbval.p |
. . . . . 6
β’ (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
11 | 1, 2, 3, 10, 6, 9 | glbeu 18127 |
. . . . 5
β’ ((π β§ π β dom πΊ) β β!π₯ β π΅ π) |
12 | | raleq 3354 |
. . . . . . . 8
β’ (π = π β (βπ¦ β π π₯ β€ π¦ β βπ¦ β π π₯ β€ π¦)) |
13 | | raleq 3354 |
. . . . . . . . . 10
β’ (π = π β (βπ¦ β π π§ β€ π¦ β βπ¦ β π π§ β€ π¦)) |
14 | 13 | imbi1d 343 |
. . . . . . . . 9
β’ (π = π β ((βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
15 | 14 | ralbidv 3171 |
. . . . . . . 8
β’ (π = π β (βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
16 | 12, 15 | anbi12d 632 |
. . . . . . 7
β’ (π = π β ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
17 | 16, 10 | bitr4di 290 |
. . . . . 6
β’ (π = π β ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β π)) |
18 | 17 | reubidv 3335 |
. . . . 5
β’ (π = π β (β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β β!π₯ β π΅ π)) |
19 | 9, 11, 18 | elabd 3617 |
. . . 4
β’ ((π β§ π β dom πΊ) β π β {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))}) |
20 | 19 | fvresd 6820 |
. . 3
β’ ((π β§ π β dom πΊ) β (((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))})βπ) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))))βπ)) |
21 | | glbval.ss |
. . . . . 6
β’ (π β π β π΅) |
22 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ π β dom πΊ) β π β π΅) |
23 | 1 | fvexi 6814 |
. . . . . 6
β’ π΅ β V |
24 | 23 | elpw2 5278 |
. . . . 5
β’ (π β π« π΅ β π β π΅) |
25 | 22, 24 | sylibr 234 |
. . . 4
β’ ((π β§ π β dom πΊ) β π β π« π΅) |
26 | 17 | riotabidv 7262 |
. . . . 5
β’ (π = π β (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) = (β©π₯ β π΅ π)) |
27 | | eqid 2736 |
. . . . 5
β’ (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) = (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
28 | | riotaex 7264 |
. . . . 5
β’
(β©π₯
β π΅ π) β V |
29 | 26, 27, 28 | fvmpt 6903 |
. . . 4
β’ (π β π« π΅ β ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))))βπ) = (β©π₯ β π΅ π)) |
30 | 25, 29 | syl 17 |
. . 3
β’ ((π β§ π β dom πΊ) β ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))))βπ) = (β©π₯ β π΅ π)) |
31 | 8, 20, 30 | 3eqtrd 2780 |
. 2
β’ ((π β§ π β dom πΊ) β (πΊβπ) = (β©π₯ β π΅ π)) |
32 | | ndmfv 6832 |
. . . 4
β’ (Β¬
π β dom πΊ β (πΊβπ) = β
) |
33 | 32 | adantl 483 |
. . 3
β’ ((π β§ Β¬ π β dom πΊ) β (πΊβπ) = β
) |
34 | 1, 2, 3, 10, 5 | glbeldm 18125 |
. . . . . . 7
β’ (π β (π β dom πΊ β (π β π΅ β§ β!π₯ β π΅ π))) |
35 | 34 | biimprd 249 |
. . . . . 6
β’ (π β ((π β π΅ β§ β!π₯ β π΅ π) β π β dom πΊ)) |
36 | 21, 35 | mpand 693 |
. . . . 5
β’ (π β (β!π₯ β π΅ π β π β dom πΊ)) |
37 | 36 | con3dimp 410 |
. . . 4
β’ ((π β§ Β¬ π β dom πΊ) β Β¬ β!π₯ β π΅ π) |
38 | | riotaund 7300 |
. . . 4
β’ (Β¬
β!π₯ β π΅ π β (β©π₯ β π΅ π) = β
) |
39 | 37, 38 | syl 17 |
. . 3
β’ ((π β§ Β¬ π β dom πΊ) β (β©π₯ β π΅ π) = β
) |
40 | 33, 39 | eqtr4d 2779 |
. 2
β’ ((π β§ Β¬ π β dom πΊ) β (πΊβπ) = (β©π₯ β π΅ π)) |
41 | 31, 40 | pm2.61dan 811 |
1
β’ (π β (πΊβπ) = (β©π₯ β π΅ π)) |