Step | Hyp | Ref
| Expression |
1 | | joindef.k |
. . . . . 6
β’ (π β πΎ β π) |
2 | | joindef.u |
. . . . . . 7
β’ π = (lubβπΎ) |
3 | | joindef.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
4 | 2, 3 | joinfval2 18327 |
. . . . . 6
β’ (πΎ β π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}) |
5 | 1, 4 | syl 17 |
. . . . 5
β’ (π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}) |
6 | 5 | oveqd 7426 |
. . . 4
β’ (π β (π β¨ π) = (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π)) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ {π, π} β dom π) β (π β¨ π) = (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π)) |
8 | | simpr 486 |
. . . 4
β’ ((π β§ {π, π} β dom π) β {π, π} β dom π) |
9 | | eqidd 2734 |
. . . 4
β’ ((π β§ {π, π} β dom π) β (πβ{π, π}) = (πβ{π, π})) |
10 | | joindef.x |
. . . . . 6
β’ (π β π β π) |
11 | | joindef.y |
. . . . . 6
β’ (π β π β π) |
12 | | fvexd 6907 |
. . . . . 6
β’ (π β (πβ{π, π}) β V) |
13 | | preq12 4740 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β {π₯, π¦} = {π, π}) |
14 | 13 | eleq1d 2819 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π) β ({π₯, π¦} β dom π β {π, π} β dom π)) |
15 | 14 | 3adant3 1133 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β ({π₯, π¦} β dom π β {π, π} β dom π)) |
16 | | simp3 1139 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β π§ = (πβ{π, π})) |
17 | 13 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π₯ = π β§ π¦ = π) β (πβ{π₯, π¦}) = (πβ{π, π})) |
18 | 17 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β (πβ{π₯, π¦}) = (πβ{π, π})) |
19 | 16, 18 | eqeq12d 2749 |
. . . . . . . 8
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β (π§ = (πβ{π₯, π¦}) β (πβ{π, π}) = (πβ{π, π}))) |
20 | 15, 19 | anbi12d 632 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π β§ π§ = (πβ{π, π})) β (({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦})) β ({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})))) |
21 | | moeq 3704 |
. . . . . . . 8
β’
β*π§ π§ = (πβ{π₯, π¦}) |
22 | 21 | moani 2548 |
. . . . . . 7
β’
β*π§({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦})) |
23 | | eqid 2733 |
. . . . . . 7
β’
{β¨β¨π₯,
π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))} = {β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))} |
24 | 20, 22, 23 | ovigg 7553 |
. . . . . 6
β’ ((π β π β§ π β π β§ (πβ{π, π}) β V) β (({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π}))) |
25 | 10, 11, 12, 24 | syl3anc 1372 |
. . . . 5
β’ (π β (({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π}))) |
26 | 25 | adantr 482 |
. . . 4
β’ ((π β§ {π, π} β dom π) β (({π, π} β dom π β§ (πβ{π, π}) = (πβ{π, π})) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π}))) |
27 | 8, 9, 26 | mp2and 698 |
. . 3
β’ ((π β§ {π, π} β dom π) β (π{β¨β¨π₯, π¦β©, π§β© β£ ({π₯, π¦} β dom π β§ π§ = (πβ{π₯, π¦}))}π) = (πβ{π, π})) |
28 | 7, 27 | eqtrd 2773 |
. 2
β’ ((π β§ {π, π} β dom π) β (π β¨ π) = (πβ{π, π})) |
29 | 2, 3, 1, 10, 11 | joindef 18329 |
. . . . . 6
β’ (π β (β¨π, πβ© β dom β¨ β {π, π} β dom π)) |
30 | 29 | notbid 318 |
. . . . 5
β’ (π β (Β¬ β¨π, πβ© β dom β¨ β Β¬ {π, π} β dom π)) |
31 | | df-ov 7412 |
. . . . . 6
β’ (π β¨ π) = ( β¨ ββ¨π, πβ©) |
32 | | ndmfv 6927 |
. . . . . 6
β’ (Β¬
β¨π, πβ© β dom β¨ β ( β¨
ββ¨π, πβ©) =
β
) |
33 | 31, 32 | eqtrid 2785 |
. . . . 5
β’ (Β¬
β¨π, πβ© β dom β¨ β (π β¨ π) = β
) |
34 | 30, 33 | syl6bir 254 |
. . . 4
β’ (π β (Β¬ {π, π} β dom π β (π β¨ π) = β
)) |
35 | 34 | imp 408 |
. . 3
β’ ((π β§ Β¬ {π, π} β dom π) β (π β¨ π) = β
) |
36 | | ndmfv 6927 |
. . . 4
β’ (Β¬
{π, π} β dom π β (πβ{π, π}) = β
) |
37 | 36 | adantl 483 |
. . 3
β’ ((π β§ Β¬ {π, π} β dom π) β (πβ{π, π}) = β
) |
38 | 35, 37 | eqtr4d 2776 |
. 2
β’ ((π β§ Β¬ {π, π} β dom π) β (π β¨ π) = (πβ{π, π})) |
39 | 28, 38 | pm2.61dan 812 |
1
β’ (π β (π β¨ π) = (πβ{π, π})) |