Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . 3
β’
(glbβπΎ) =
(glbβπΎ) |
2 | | meetval2.m |
. . 3
β’ β§ =
(meetβπΎ) |
3 | | meetval2.k |
. . 3
β’ (π β πΎ β π) |
4 | | meetval2.x |
. . 3
β’ (π β π β π΅) |
5 | | meetval2.y |
. . 3
β’ (π β π β π΅) |
6 | 1, 2, 3, 4, 5 | meetval 18150 |
. 2
β’ (π β (π β§ π) = ((glbβπΎ)β{π, π})) |
7 | | meetval2.b |
. . 3
β’ π΅ = (BaseβπΎ) |
8 | | meetval2.l |
. . 3
β’ β€ =
(leβπΎ) |
9 | | biid 262 |
. . 3
β’
((βπ¦ β
{π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯)) β (βπ¦ β {π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯))) |
10 | 4, 5 | prssd 4761 |
. . 3
β’ (π β {π, π} β π΅) |
11 | 7, 8, 1, 9, 3, 10 | glbval 18128 |
. 2
β’ (π β ((glbβπΎ)β{π, π}) = (β©π₯ β π΅ (βπ¦ β {π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯)))) |
12 | 7, 8, 2, 3, 4, 5 | meetval2lem 18153 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β ((βπ¦ β {π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯)) β ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) |
13 | 12 | riotabidv 7262 |
. . 3
β’ ((π β π΅ β§ π β π΅) β (β©π₯ β π΅ (βπ¦ β {π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯))) = (β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) |
14 | 4, 5, 13 | syl2anc 585 |
. 2
β’ (π β (β©π₯ β π΅ (βπ¦ β {π, π}π₯ β€ π¦ β§ βπ§ β π΅ (βπ¦ β {π, π}π§ β€ π¦ β π§ β€ π₯))) = (β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) |
15 | 6, 11, 14 | 3eqtrd 2780 |
1
β’ (π β (π β§ π) = (β©π₯ β π΅ ((π₯ β€ π β§ π₯ β€ π) β§ βπ§ β π΅ ((π§ β€ π β§ π§ β€ π) β π§ β€ π₯)))) |