Step | Hyp | Ref
| Expression |
1 | | relopabv 5778 |
. . 3
β’ Rel
{β¨π₯, π¦β© β£ {π₯, π¦} β dom (glbβπΎ)} |
2 | | meetdmss.k |
. . . . 5
β’ (π β πΎ β π) |
3 | | eqid 2733 |
. . . . . 6
β’
(glbβπΎ) =
(glbβπΎ) |
4 | | meetdmss.j |
. . . . . 6
β’ β§ =
(meetβπΎ) |
5 | 3, 4 | meetdm 18283 |
. . . . 5
β’ (πΎ β π β dom β§ = {β¨π₯, π¦β© β£ {π₯, π¦} β dom (glbβπΎ)}) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (π β dom β§ = {β¨π₯, π¦β© β£ {π₯, π¦} β dom (glbβπΎ)}) |
7 | 6 | releqd 5735 |
. . 3
β’ (π β (Rel dom β§ β
Rel {β¨π₯, π¦β© β£ {π₯, π¦} β dom (glbβπΎ)})) |
8 | 1, 7 | mpbiri 258 |
. 2
β’ (π β Rel dom β§ ) |
9 | | vex 3448 |
. . . . 5
β’ π₯ β V |
10 | 9 | a1i 11 |
. . . 4
β’ (π β π₯ β V) |
11 | | vex 3448 |
. . . . 5
β’ π¦ β V |
12 | 11 | a1i 11 |
. . . 4
β’ (π β π¦ β V) |
13 | 3, 4, 2, 10, 12 | meetdef 18284 |
. . 3
β’ (π β (β¨π₯, π¦β© β dom β§ β {π₯, π¦} β dom (glbβπΎ))) |
14 | | meetdmss.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
15 | | eqid 2733 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
16 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ {π₯, π¦} β dom (glbβπΎ)) β πΎ β π) |
17 | | simpr 486 |
. . . . . 6
β’ ((π β§ {π₯, π¦} β dom (glbβπΎ)) β {π₯, π¦} β dom (glbβπΎ)) |
18 | 14, 15, 3, 16, 17 | glbelss 18261 |
. . . . 5
β’ ((π β§ {π₯, π¦} β dom (glbβπΎ)) β {π₯, π¦} β π΅) |
19 | 18 | ex 414 |
. . . 4
β’ (π β ({π₯, π¦} β dom (glbβπΎ) β {π₯, π¦} β π΅)) |
20 | 9, 11 | prss 4781 |
. . . . 5
β’ ((π₯ β π΅ β§ π¦ β π΅) β {π₯, π¦} β π΅) |
21 | | opelxpi 5671 |
. . . . 5
β’ ((π₯ β π΅ β§ π¦ β π΅) β β¨π₯, π¦β© β (π΅ Γ π΅)) |
22 | 20, 21 | sylbir 234 |
. . . 4
β’ ({π₯, π¦} β π΅ β β¨π₯, π¦β© β (π΅ Γ π΅)) |
23 | 19, 22 | syl6 35 |
. . 3
β’ (π β ({π₯, π¦} β dom (glbβπΎ) β β¨π₯, π¦β© β (π΅ Γ π΅))) |
24 | 13, 23 | sylbid 239 |
. 2
β’ (π β (β¨π₯, π¦β© β dom β§ β β¨π₯, π¦β© β (π΅ Γ π΅))) |
25 | 8, 24 | relssdv 5745 |
1
β’ (π β dom β§ β (π΅ Γ π΅)) |