Step | Hyp | Ref
| Expression |
1 | | elex 3462 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | joinfval.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | fvex 6856 |
. . . . . . 7
β’
(BaseβπΎ)
β V |
4 | | moeq 3666 |
. . . . . . . 8
β’
β*π§ π§ = (πβ{π₯, π¦}) |
5 | 4 | a1i 11 |
. . . . . . 7
β’ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β β*π§ π§ = (πβ{π₯, π¦})) |
6 | | eqid 2733 |
. . . . . . 7
β’
{β¨β¨π₯,
π¦β©, π§β© β£ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))} = {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))} |
7 | 3, 3, 5, 6 | oprabex 7910 |
. . . . . 6
β’
{β¨β¨π₯,
π¦β©, π§β© β£ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))} β V |
8 | 7 | a1i 11 |
. . . . 5
β’ (πΎ β V β
{β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))} β V) |
9 | | joinfval.u |
. . . . . . . . . . . 12
β’ π = (lubβπΎ) |
10 | 9 | lubfun 18246 |
. . . . . . . . . . 11
β’ Fun π |
11 | | funbrfv2b 6901 |
. . . . . . . . . . 11
β’ (Fun
π β ({π₯, π¦}ππ§ β ({π₯, π¦} β dom π β§ (πβ{π₯, π¦}) = π§))) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . . 10
β’ ({π₯, π¦}ππ§ β ({π₯, π¦} β dom π β§ (πβ{π₯, π¦}) = π§)) |
13 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(BaseβπΎ) =
(BaseβπΎ) |
14 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(leβπΎ) =
(leβπΎ) |
15 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((πΎ β V β§ {π₯, π¦} β dom π) β πΎ β V) |
16 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((πΎ β V β§ {π₯, π¦} β dom π) β {π₯, π¦} β dom π) |
17 | 13, 14, 9, 15, 16 | lubelss 18248 |
. . . . . . . . . . . . 13
β’ ((πΎ β V β§ {π₯, π¦} β dom π) β {π₯, π¦} β (BaseβπΎ)) |
18 | 17 | ex 414 |
. . . . . . . . . . . 12
β’ (πΎ β V β ({π₯, π¦} β dom π β {π₯, π¦} β (BaseβπΎ))) |
19 | | vex 3448 |
. . . . . . . . . . . . 13
β’ π₯ β V |
20 | | vex 3448 |
. . . . . . . . . . . . 13
β’ π¦ β V |
21 | 19, 20 | prss 4781 |
. . . . . . . . . . . 12
β’ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β {π₯, π¦} β (BaseβπΎ)) |
22 | 18, 21 | syl6ibr 252 |
. . . . . . . . . . 11
β’ (πΎ β V β ({π₯, π¦} β dom π β (π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)))) |
23 | | eqcom 2740 |
. . . . . . . . . . . 12
β’ ((πβ{π₯, π¦}) = π§ β π§ = (πβ{π₯, π¦})) |
24 | 23 | biimpi 215 |
. . . . . . . . . . 11
β’ ((πβ{π₯, π¦}) = π§ β π§ = (πβ{π₯, π¦})) |
25 | 22, 24 | anim12d1 611 |
. . . . . . . . . 10
β’ (πΎ β V β (({π₯, π¦} β dom π β§ (πβ{π₯, π¦}) = π§) β ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦})))) |
26 | 12, 25 | biimtrid 241 |
. . . . . . . . 9
β’ (πΎ β V β ({π₯, π¦}ππ§ β ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦})))) |
27 | 26 | alrimiv 1931 |
. . . . . . . 8
β’ (πΎ β V β βπ§({π₯, π¦}ππ§ β ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦})))) |
28 | 27 | alrimiv 1931 |
. . . . . . 7
β’ (πΎ β V β βπ¦βπ§({π₯, π¦}ππ§ β ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦})))) |
29 | 28 | alrimiv 1931 |
. . . . . 6
β’ (πΎ β V β βπ₯βπ¦βπ§({π₯, π¦}ππ§ β ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦})))) |
30 | | ssoprab2 7426 |
. . . . . 6
β’
(βπ₯βπ¦βπ§({π₯, π¦}ππ§ β ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))) β {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§} β {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))}) |
31 | 29, 30 | syl 17 |
. . . . 5
β’ (πΎ β V β
{β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§} β {β¨β¨π₯, π¦β©, π§β© β£ ((π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ)) β§ π§ = (πβ{π₯, π¦}))}) |
32 | 8, 31 | ssexd 5282 |
. . . 4
β’ (πΎ β V β
{β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§} β V) |
33 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (lubβπ) = (lubβπΎ)) |
34 | 33, 9 | eqtr4di 2791 |
. . . . . . 7
β’ (π = πΎ β (lubβπ) = π) |
35 | 34 | breqd 5117 |
. . . . . 6
β’ (π = πΎ β ({π₯, π¦} (lubβπ)π§ β {π₯, π¦}ππ§)) |
36 | 35 | oprabbidv 7424 |
. . . . 5
β’ (π = πΎ β {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦} (lubβπ)π§} = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§}) |
37 | | df-join 18242 |
. . . . 5
β’ join =
(π β V β¦
{β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦} (lubβπ)π§}) |
38 | 36, 37 | fvmptg 6947 |
. . . 4
β’ ((πΎ β V β§
{β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§} β V) β (joinβπΎ) = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§}) |
39 | 32, 38 | mpdan 686 |
. . 3
β’ (πΎ β V β
(joinβπΎ) =
{β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§}) |
40 | 2, 39 | eqtrid 2785 |
. 2
β’ (πΎ β V β β¨ =
{β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§}) |
41 | 1, 40 | syl 17 |
1
β’ (πΎ β π β β¨ = {β¨β¨π₯, π¦β©, π§β© β£ {π₯, π¦}ππ§}) |