Step | Hyp | Ref
| Expression |
1 | | lubval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | lubval.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | lubval.u |
. . . . 5
β’ π = (lubβπΎ) |
4 | | biid 261 |
. . . . 5
β’
((βπ¦ β
π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
5 | | lubval.k |
. . . . . 6
β’ (π β πΎ β π) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π β dom π) β πΎ β π) |
7 | 1, 2, 3, 4, 6 | lubfval 18247 |
. . . 4
β’ ((π β§ π β dom π) β π = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))})) |
8 | 7 | fveq1d 6848 |
. . 3
β’ ((π β§ π β dom π) β (πβπ) = (((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))})βπ)) |
9 | | simpr 486 |
. . . . 5
β’ ((π β§ π β dom π) β π β dom π) |
10 | | lubval.p |
. . . . . 6
β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
11 | 1, 2, 3, 10, 6, 9 | lubeu 18252 |
. . . . 5
β’ ((π β§ π β dom π) β β!π₯ β π΅ π) |
12 | | raleq 3308 |
. . . . . . . 8
β’ (π = π β (βπ¦ β π π¦ β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
13 | | raleq 3308 |
. . . . . . . . . 10
β’ (π = π β (βπ¦ β π π¦ β€ π§ β βπ¦ β π π¦ β€ π§)) |
14 | 13 | imbi1d 342 |
. . . . . . . . 9
β’ (π = π β ((βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
15 | 14 | ralbidv 3171 |
. . . . . . . 8
β’ (π = π β (βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
16 | 12, 15 | anbi12d 632 |
. . . . . . 7
β’ (π = π β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
17 | 16, 10 | bitr4di 289 |
. . . . . 6
β’ (π = π β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β π)) |
18 | 17 | reubidv 3370 |
. . . . 5
β’ (π = π β (β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β β!π₯ β π΅ π)) |
19 | 9, 11, 18 | elabd 3637 |
. . . 4
β’ ((π β§ π β dom π) β π β {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))}) |
20 | 19 | fvresd 6866 |
. . 3
β’ ((π β§ π β dom π) β (((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) βΎ {π β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))})βπ) = ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))))βπ)) |
21 | | lubval.s |
. . . . . 6
β’ (π β π β π΅) |
22 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ π β dom π) β π β π΅) |
23 | 1 | fvexi 6860 |
. . . . . 6
β’ π΅ β V |
24 | 23 | elpw2 5306 |
. . . . 5
β’ (π β π« π΅ β π β π΅) |
25 | 22, 24 | sylibr 233 |
. . . 4
β’ ((π β§ π β dom π) β π β π« π΅) |
26 | 17 | riotabidv 7319 |
. . . . 5
β’ (π = π β (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) = (β©π₯ β π΅ π)) |
27 | | eqid 2733 |
. . . . 5
β’ (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) = (π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
28 | | riotaex 7321 |
. . . . 5
β’
(β©π₯
β π΅ π) β V |
29 | 26, 27, 28 | fvmpt 6952 |
. . . 4
β’ (π β π« π΅ β ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))))βπ) = (β©π₯ β π΅ π)) |
30 | 25, 29 | syl 17 |
. . 3
β’ ((π β§ π β dom π) β ((π β π« π΅ β¦ (β©π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))))βπ) = (β©π₯ β π΅ π)) |
31 | 8, 20, 30 | 3eqtrd 2777 |
. 2
β’ ((π β§ π β dom π) β (πβπ) = (β©π₯ β π΅ π)) |
32 | | ndmfv 6881 |
. . . 4
β’ (Β¬
π β dom π β (πβπ) = β
) |
33 | 32 | adantl 483 |
. . 3
β’ ((π β§ Β¬ π β dom π) β (πβπ) = β
) |
34 | 1, 2, 3, 10, 5 | lubeldm 18250 |
. . . . . . 7
β’ (π β (π β dom π β (π β π΅ β§ β!π₯ β π΅ π))) |
35 | 34 | biimprd 248 |
. . . . . 6
β’ (π β ((π β π΅ β§ β!π₯ β π΅ π) β π β dom π)) |
36 | 21, 35 | mpand 694 |
. . . . 5
β’ (π β (β!π₯ β π΅ π β π β dom π)) |
37 | 36 | con3dimp 410 |
. . . 4
β’ ((π β§ Β¬ π β dom π) β Β¬ β!π₯ β π΅ π) |
38 | | riotaund 7357 |
. . . 4
β’ (Β¬
β!π₯ β π΅ π β (β©π₯ β π΅ π) = β
) |
39 | 37, 38 | syl 17 |
. . 3
β’ ((π β§ Β¬ π β dom π) β (β©π₯ β π΅ π) = β
) |
40 | 33, 39 | eqtr4d 2776 |
. 2
β’ ((π β§ Β¬ π β dom π) β (πβπ) = (β©π₯ β π΅ π)) |
41 | 31, 40 | pm2.61dan 812 |
1
β’ (π β (πβπ) = (β©π₯ β π΅ π)) |