Step | Hyp | Ref
| Expression |
1 | | meetdef.k |
. . . . . 6
β’ (π β πΎ β π) |
2 | | meetdef.u |
. . . . . . 7
β’ πΊ = (glbβπΎ) |
3 | | meetdef.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
4 | 2, 3 | meetfval2 18147 |
. . . . . 6
β’ (πΎ β π β β§ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β β§ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}) |
6 | 5 | oveqd 7320 |
. . . 4
β’ (π β (π β§ π) = (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}π)) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ {π, π} β dom πΊ) β (π β§ π) = (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}π)) |
8 | | simpr 486 |
. . . 4
β’ ((π β§ {π, π} β dom πΊ) β {π, π} β dom πΊ) |
9 | | eqidd 2737 |
. . . 4
β’ ((π β§ {π, π} β dom πΊ) β (πΊβ{π, π}) = (πΊβ{π, π})) |
10 | | meetdef.x |
. . . . . 6
β’ (π β π β π) |
11 | | meetdef.y |
. . . . . 6
β’ (π β π β π) |
12 | | fvexd 6815 |
. . . . . 6
β’ (π β (πΊβ{π, π}) β V) |
13 | | preq12 4675 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β {π₯, π¦} = {π, π}) |
14 | 13 | eleq1d 2821 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β ({π₯, π¦} β dom πΊ β {π, π} β dom πΊ)) |
15 | 14 | 3adant3 1132 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πΊβ{π, π})) β ({π₯, π¦} β dom πΊ β {π, π} β dom πΊ)) |
16 | | simp3 1138 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πΊβ{π, π})) β π§ = (πΊβ{π, π})) |
17 | 13 | fveq2d 6804 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β (πΊβ{π₯, π¦}) = (πΊβ{π, π})) |
18 | 17 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πΊβ{π, π})) β (πΊβ{π₯, π¦}) = (πΊβ{π, π})) |
19 | 16, 18 | eqeq12d 2752 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πΊβ{π, π})) β (π§ = (πΊβ{π₯, π¦}) β (πΊβ{π, π}) = (πΊβ{π, π}))) |
20 | 15, 19 | anbi12d 632 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πΊβ{π, π})) β (({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦})) β ({π, π} β dom πΊ β§ (πΊβ{π, π}) = (πΊβ{π, π})))) |
21 | | moeq 3647 |
. . . . . . . 8
β’
β*π§ π§ = (πΊβ{π₯, π¦}) |
22 | 21 | moani 2551 |
. . . . . . 7
β’
β*π§({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦})) |
23 | | eqid 2736 |
. . . . . . 7
β’
{β¨β¨π₯,
π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))} = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))} |
24 | 20, 22, 23 | ovigg 7446 |
. . . . . 6
β’ ((π β π β§ π β π β§ (πΊβ{π, π}) β V) β (({π, π} β dom πΊ β§ (πΊβ{π, π}) = (πΊβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}π) = (πΊβ{π, π}))) |
25 | 10, 11, 12, 24 | syl3anc 1371 |
. . . . 5
β’ (π β (({π, π} β dom πΊ β§ (πΊβ{π, π}) = (πΊβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}π) = (πΊβ{π, π}))) |
26 | 25 | adantr 482 |
. . . 4
β’ ((π β§ {π, π} β dom πΊ) β (({π, π} β dom πΊ β§ (πΊβ{π, π}) = (πΊβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}π) = (πΊβ{π, π}))) |
27 | 8, 9, 26 | mp2and 697 |
. . 3
β’ ((π β§ {π, π} β dom πΊ) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom πΊ β§ π§ = (πΊβ{π₯, π¦}))}π) = (πΊβ{π, π})) |
28 | 7, 27 | eqtrd 2776 |
. 2
β’ ((π β§ {π, π} β dom πΊ) β (π β§ π) = (πΊβ{π, π})) |
29 | 2, 3, 1, 10, 11 | meetdef 18149 |
. . . . . 6
β’ (π β (β¨π, πβ© β dom β§ β {π, π} β dom πΊ)) |
30 | 29 | notbid 319 |
. . . . 5
β’ (π β (Β¬ β¨π, πβ© β dom β§ β Β¬ {π, π} β dom πΊ)) |
31 | | df-ov 7306 |
. . . . . 6
β’ (π β§ π) = ( β§ ββ¨π, πβ©) |
32 | | ndmfv 6832 |
. . . . . 6
β’ (Β¬
β¨π, πβ© β dom β§ β ( β§
ββ¨π, πβ©) =
β
) |
33 | 31, 32 | eqtrid 2788 |
. . . . 5
β’ (Β¬
β¨π, πβ© β dom β§ β (π β§ π) = β
) |
34 | 30, 33 | syl6bir 255 |
. . . 4
β’ (π β (Β¬ {π, π} β dom πΊ β (π β§ π) = β
)) |
35 | 34 | imp 408 |
. . 3
β’ ((π β§ Β¬ {π, π} β dom πΊ) β (π β§ π) = β
) |
36 | | ndmfv 6832 |
. . . 4
β’ (Β¬
{π, π} β dom πΊ β (πΊβ{π, π}) = β
) |
37 | 36 | adantl 483 |
. . 3
β’ ((π β§ Β¬ {π, π} β dom πΊ) β (πΊβ{π, π}) = β
) |
38 | 35, 37 | eqtr4d 2779 |
. 2
β’ ((π β§ Β¬ {π, π} β dom πΊ) β (π β§ π) = (πΊβ{π, π})) |
39 | 28, 38 | pm2.61dan 811 |
1
β’ (π β (π β§ π) = (πΊβ{π, π})) |