Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | eqid 2726 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
3 | | eqid 2726 |
. . 3
β’
(glbβπΎ) =
(glbβπΎ) |
4 | | biid 261 |
. . 3
β’
((βπ¦ β
π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯)) β (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) |
5 | | glbeldm2d.k |
. . 3
β’ (π β πΎ β Poset) |
6 | 1, 2, 3, 4, 5 | glbeldm2 47864 |
. 2
β’ (π β (π β dom (glbβπΎ) β (π β (BaseβπΎ) β§ βπ₯ β (BaseβπΎ)(βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))))) |
7 | | glbeldm2d.g |
. . . 4
β’ (π β πΊ = (glbβπΎ)) |
8 | 7 | dmeqd 5899 |
. . 3
β’ (π β dom πΊ = dom (glbβπΎ)) |
9 | 8 | eleq2d 2813 |
. 2
β’ (π β (π β dom πΊ β π β dom (glbβπΎ))) |
10 | | lubeldm2d.b |
. . . 4
β’ (π β π΅ = (BaseβπΎ)) |
11 | 10 | sseq2d 4009 |
. . 3
β’ (π β (π β π΅ β π β (BaseβπΎ))) |
12 | | glbeldm2d.p |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β (π β (βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)))) |
13 | | lubeldm2d.l |
. . . . . . . . . . 11
β’ (π β β€ = (leβπΎ)) |
14 | 13 | breqd 5152 |
. . . . . . . . . 10
β’ (π β (π₯ β€ π¦ β π₯(leβπΎ)π¦)) |
15 | 14 | ralbidv 3171 |
. . . . . . . . 9
β’ (π β (βπ¦ β π π₯ β€ π¦ β βπ¦ β π π₯(leβπΎ)π¦)) |
16 | 13 | breqd 5152 |
. . . . . . . . . . . 12
β’ (π β (π§ β€ π¦ β π§(leβπΎ)π¦)) |
17 | 16 | ralbidv 3171 |
. . . . . . . . . . 11
β’ (π β (βπ¦ β π π§ β€ π¦ β βπ¦ β π π§(leβπΎ)π¦)) |
18 | 13 | breqd 5152 |
. . . . . . . . . . 11
β’ (π β (π§ β€ π₯ β π§(leβπΎ)π₯)) |
19 | 17, 18 | imbi12d 344 |
. . . . . . . . . 10
β’ (π β ((βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β (βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) |
20 | 10, 19 | raleqbidv 3336 |
. . . . . . . . 9
β’ (π β (βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯) β βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) |
21 | 15, 20 | anbi12d 630 |
. . . . . . . 8
β’ (π β ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯)))) |
22 | 21 | adantr 480 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β ((βπ¦ β π π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β π π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯)))) |
23 | 12, 22 | bitrd 279 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β (π β (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯)))) |
24 | 23 | pm5.32da 578 |
. . . . 5
β’ (π β ((π₯ β π΅ β§ π) β (π₯ β π΅ β§ (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))))) |
25 | 10 | eleq2d 2813 |
. . . . . 6
β’ (π β (π₯ β π΅ β π₯ β (BaseβπΎ))) |
26 | 25 | anbi1d 629 |
. . . . 5
β’ (π β ((π₯ β π΅ β§ (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))) β (π₯ β (BaseβπΎ) β§ (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))))) |
27 | 24, 26 | bitrd 279 |
. . . 4
β’ (π β ((π₯ β π΅ β§ π) β (π₯ β (BaseβπΎ) β§ (βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))))) |
28 | 27 | rexbidv2 3168 |
. . 3
β’ (π β (βπ₯ β π΅ π β βπ₯ β (BaseβπΎ)(βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯)))) |
29 | 11, 28 | anbi12d 630 |
. 2
β’ (π β ((π β π΅ β§ βπ₯ β π΅ π) β (π β (BaseβπΎ) β§ βπ₯ β (BaseβπΎ)(βπ¦ β π π₯(leβπΎ)π¦ β§ βπ§ β (BaseβπΎ)(βπ¦ β π π§(leβπΎ)π¦ β π§(leβπΎ)π₯))))) |
30 | 6, 9, 29 | 3bitr4d 311 |
1
β’ (π β (π β dom πΊ β (π β π΅ β§ βπ₯ β π΅ π))) |