Step | Hyp | Ref
| Expression |
1 | | lubeldm.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | lubeldm.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | lubeldm.u |
. . . 4
β’ π = (lubβπΎ) |
4 | | biid 261 |
. . . 4
β’
((βπ¦ β
π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
5 | | lubeldm.k |
. . . 4
β’ (π β πΎ β π) |
6 | 1, 2, 3, 4, 5 | lubdm 18248 |
. . 3
β’ (π β dom π = {π β π« π΅ β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))}) |
7 | 6 | eleq2d 2820 |
. 2
β’ (π β (π β dom π β π β {π β π« π΅ β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))})) |
8 | | raleq 3308 |
. . . . . . 7
β’ (π = π β (βπ¦ β π π¦ β€ π₯ β βπ¦ β π π¦ β€ π₯)) |
9 | | raleq 3308 |
. . . . . . . . 9
β’ (π = π β (βπ¦ β π π¦ β€ π§ β βπ¦ β π π¦ β€ π§)) |
10 | 9 | imbi1d 342 |
. . . . . . . 8
β’ (π = π β ((βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
11 | 10 | ralbidv 3171 |
. . . . . . 7
β’ (π = π β (βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§) β βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
12 | 8, 11 | anbi12d 632 |
. . . . . 6
β’ (π = π β ((βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
13 | 12 | reubidv 3370 |
. . . . 5
β’ (π = π β (β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)))) |
14 | | lubeldm.p |
. . . . . 6
β’ (π β (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
15 | 14 | reubii 3361 |
. . . . 5
β’
(β!π₯ β
π΅ π β β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))) |
16 | 13, 15 | bitr4di 289 |
. . . 4
β’ (π = π β (β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§)) β β!π₯ β π΅ π)) |
17 | 16 | elrab 3649 |
. . 3
β’ (π β {π β π« π΅ β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))} β (π β π« π΅ β§ β!π₯ β π΅ π)) |
18 | 1 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
19 | 18 | elpw2 5306 |
. . . 4
β’ (π β π« π΅ β π β π΅) |
20 | 19 | anbi1i 625 |
. . 3
β’ ((π β π« π΅ β§ β!π₯ β π΅ π) β (π β π΅ β§ β!π₯ β π΅ π)) |
21 | 17, 20 | bitri 275 |
. 2
β’ (π β {π β π« π΅ β£ β!π₯ β π΅ (βπ¦ β π π¦ β€ π₯ β§ βπ§ β π΅ (βπ¦ β π π¦ β€ π§ β π₯ β€ π§))} β (π β π΅ β§ β!π₯ β π΅ π)) |
22 | 7, 21 | bitrdi 287 |
1
β’ (π β (π β dom π β (π β π΅ β§ β!π₯ β π΅ π))) |