Step | Hyp | Ref
| Expression |
1 | | joindef.k |
. . . . . 6
β’ (π β πΎ β π) |
2 | | joindef.u |
. . . . . . 7
β’ π = (lubβπΎ) |
3 | | joindef.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
4 | 2, 3 | joinfval2 18323 |
. . . . . 6
β’ (πΎ β π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}) |
6 | 5 | oveqd 7422 |
. . . 4
β’ (π β (π β¨ π) = (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π)) |
7 | 6 | adantr 481 |
. . 3
β’ ((π β§ {π, π} β dom π) β (π β¨ π) = (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π)) |
8 | | simpr 485 |
. . . 4
β’ ((π β§ {π, π} β dom π) β {π, π} β dom π) |
9 | | eqidd 2733 |
. . . 4
β’ ((π β§ {π, π} β dom π) β (πβ{π, π}) = (πβ{π, π})) |
10 | | joindef.x |
. . . . . 6
β’ (π β π β π) |
11 | | joindef.y |
. . . . . 6
β’ (π β π β π) |
12 | | fvexd 6903 |
. . . . . 6
β’ (π β (πβ{π, π}) β V) |
13 | | preq12 4738 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β {π₯, π¦} = {π, π}) |
14 | 13 | eleq1d 2818 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β ({π₯, π¦} β dom π β {π, π} β dom π)) |
15 | 14 | 3adant3 1132 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β ({π₯, π¦} β dom π β {π, π} β dom π)) |
16 | | simp3 1138 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β π§ = (πβ{π, π})) |
17 | 13 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β (πβ{π₯, π¦}) = (πβ{π, π})) |
18 | 17 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β (πβ{π₯, π¦}) = (πβ{π, π})) |
19 | 16, 18 | eqeq12d 2748 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β (π§ = (πβ{π₯, π¦}) β (πβ{π, π}) = (πβ{π, π}))) |
20 | 15, 19 | anbi12d 631 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β (({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦})) β ({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})))) |
21 | | moeq 3702 |
. . . . . . . 8
β’
β*π§ π§ = (πβ{π₯, π¦}) |
22 | 21 | moani 2547 |
. . . . . . 7
β’
β*π§({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦})) |
23 | | eqid 2732 |
. . . . . . 7
β’
{β¨β¨π₯,
π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))} = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))} |
24 | 20, 22, 23 | ovigg 7549 |
. . . . . 6
β’ ((π β π β§ π β π β§ (πβ{π, π}) β V) β (({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π}))) |
25 | 10, 11, 12, 24 | syl3anc 1371 |
. . . . 5
β’ (π β (({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π}))) |
26 | 25 | adantr 481 |
. . . 4
β’ ((π β§ {π, π} β dom π) β (({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π}))) |
27 | 8, 9, 26 | mp2and 697 |
. . 3
β’ ((π β§ {π, π} β dom π) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π})) |
28 | 7, 27 | eqtrd 2772 |
. 2
β’ ((π β§ {π, π} β dom π) β (π β¨ π) = (πβ{π, π})) |
29 | 2, 3, 1, 10, 11 | joindef 18325 |
. . . . . 6
β’ (π β (β¨π, πβ© β dom β¨ β {π, π} β dom π)) |
30 | 29 | notbid 317 |
. . . . 5
β’ (π β (Β¬ β¨π, πβ© β dom β¨ β Β¬ {π, π} β dom π)) |
31 | | df-ov 7408 |
. . . . . 6
β’ (π β¨ π) = ( β¨ ββ¨π, πβ©) |
32 | | ndmfv 6923 |
. . . . . 6
β’ (Β¬
β¨π, πβ© β dom β¨ β ( β¨
ββ¨π, πβ©) =
β
) |
33 | 31, 32 | eqtrid 2784 |
. . . . 5
β’ (Β¬
β¨π, πβ© β dom β¨ β (π β¨ π) = β
) |
34 | 30, 33 | syl6bir 253 |
. . . 4
β’ (π β (Β¬ {π, π} β dom π β (π β¨ π) = β
)) |
35 | 34 | imp 407 |
. . 3
β’ ((π β§ Β¬ {π, π} β dom π) β (π β¨ π) = β
) |
36 | | ndmfv 6923 |
. . . 4
β’ (Β¬
{π, π} β dom π β (πβ{π, π}) = β
) |
37 | 36 | adantl 482 |
. . 3
β’ ((π β§ Β¬ {π, π} β dom π) β (πβ{π, π}) = β
) |
38 | 35, 37 | eqtr4d 2775 |
. 2
β’ ((π β§ Β¬ {π, π} β dom π) β (π β¨ π) = (πβ{π, π})) |
39 | 28, 38 | pm2.61dan 811 |
1
β’ (π β (π β¨ π) = (πβ{π, π})) |