Step | Hyp | Ref
| Expression |
1 | | glbeldm.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | glbeldm.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | glbeldm.g |
. . . 4
β’ πΊ = (glbβπΎ) |
4 | | biid 261 |
. . . 4
β’
((βπ¦ β
π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯))) |
5 | | glbeldm.k |
. . . 4
β’ (π β πΎ β π) |
6 | 1, 2, 3, 4, 5 | glbdm 18261 |
. . 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 | | glbeldm.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 πΊ β (π β π΅ β§ β!π₯ β π΅ π))) |