Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
β’ (πΎ β π΅ β πΎ β V) |
2 | | paddfval.p |
. . 3
β’ + =
(+πβπΎ) |
3 | | fveq2 6839 |
. . . . . . 7
β’ (β = πΎ β (Atomsββ) = (AtomsβπΎ)) |
4 | | paddfval.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . . 6
β’ (β = πΎ β (Atomsββ) = π΄) |
6 | 5 | pweqd 4575 |
. . . . 5
β’ (β = πΎ β π« (Atomsββ) = π« π΄) |
7 | | eqidd 2738 |
. . . . . . . . 9
β’ (β = πΎ β π = π) |
8 | | fveq2 6839 |
. . . . . . . . . 10
β’ (β = πΎ β (leββ) = (leβπΎ)) |
9 | | paddfval.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . . . 9
β’ (β = πΎ β (leββ) = β€ ) |
11 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (β = πΎ β (joinββ) = (joinβπΎ)) |
12 | | paddfval.j |
. . . . . . . . . . 11
β’ β¨ =
(joinβπΎ) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (β = πΎ β (joinββ) = β¨ ) |
14 | 13 | oveqd 7368 |
. . . . . . . . 9
β’ (β = πΎ β (π(joinββ)π) = (π β¨ π)) |
15 | 7, 10, 14 | breq123d 5117 |
. . . . . . . 8
β’ (β = πΎ β (π(leββ)(π(joinββ)π) β π β€ (π β¨ π))) |
16 | 15 | 2rexbidv 3211 |
. . . . . . 7
β’ (β = πΎ β (βπ β π βπ β π π(leββ)(π(joinββ)π) β βπ β π βπ β π π β€ (π β¨ π))) |
17 | 5, 16 | rabeqbidv 3422 |
. . . . . 6
β’ (β = πΎ β {π β (Atomsββ) β£ βπ β π βπ β π π(leββ)(π(joinββ)π)} = {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) |
18 | 17 | uneq2d 4121 |
. . . . 5
β’ (β = πΎ β ((π βͺ π) βͺ {π β (Atomsββ) β£ βπ β π βπ β π π(leββ)(π(joinββ)π)}) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
19 | 6, 6, 18 | mpoeq123dv 7426 |
. . . 4
β’ (β = πΎ β (π β π« (Atomsββ), π β π« (Atomsββ) β¦ ((π βͺ π) βͺ {π β (Atomsββ) β£ βπ β π βπ β π π(leββ)(π(joinββ)π)})) = (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))) |
20 | | df-padd 38197 |
. . . 4
β’
+π = (β β V β¦ (π β π« (Atomsββ), π β π« (Atomsββ) β¦ ((π βͺ π) βͺ {π β (Atomsββ) β£ βπ β π βπ β π π(leββ)(π(joinββ)π)}))) |
21 | 4 | fvexi 6853 |
. . . . . 6
β’ π΄ β V |
22 | 21 | pwex 5333 |
. . . . 5
β’ π«
π΄ β V |
23 | 22, 22 | mpoex 8004 |
. . . 4
β’ (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) β V |
24 | 19, 20, 23 | fvmpt 6945 |
. . 3
β’ (πΎ β V β
(+πβπΎ) = (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))) |
25 | 2, 24 | eqtrid 2789 |
. 2
β’ (πΎ β V β + = (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))) |
26 | 1, 25 | syl 17 |
1
β’ (πΎ β π΅ β + = (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))) |