Step | Hyp | Ref
| Expression |
1 | | id 22 |
. 2
β’ (π β OutMeas β π β
OutMeas) |
2 | | dmexg 7845 |
. . . . 5
β’ (π β OutMeas β dom π β V) |
3 | 2 | uniexd 7684 |
. . . 4
β’ (π β OutMeas β βͺ dom π β V) |
4 | 3 | pwexd 5339 |
. . 3
β’ (π β OutMeas β π«
βͺ dom π β V) |
5 | | rabexg 5293 |
. . 3
β’
(π« βͺ dom π β V β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) |
6 | 4, 5 | syl 17 |
. 2
β’ (π β OutMeas β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) |
7 | | dmeq 5864 |
. . . . . 6
β’ (π = π β dom π = dom π) |
8 | 7 | unieqd 4884 |
. . . . 5
β’ (π = π β βͺ dom
π = βͺ dom π) |
9 | 8 | pweqd 4582 |
. . . 4
β’ (π = π β π« βͺ dom π = π« βͺ dom
π) |
10 | 9 | raleqdv 3316 |
. . . . 5
β’ (π = π β (βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
11 | | fveq1 6846 |
. . . . . . . 8
β’ (π = π β (πβ(π β© π)) = (πβ(π β© π))) |
12 | | fveq1 6846 |
. . . . . . . 8
β’ (π = π β (πβ(π β π)) = (πβ(π β π))) |
13 | 11, 12 | oveq12d 7380 |
. . . . . . 7
β’ (π = π β ((πβ(π β© π)) +π (πβ(π β π))) = ((πβ(π β© π)) +π (πβ(π β π)))) |
14 | | fveq1 6846 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
15 | 13, 14 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
16 | 15 | ralbidv 3175 |
. . . . 5
β’ (π = π β (βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
17 | 10, 16 | bitrd 279 |
. . . 4
β’ (π = π β (βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
18 | 9, 17 | rabeqbidv 3427 |
. . 3
β’ (π = π β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
19 | | df-caragen 44807 |
. . 3
β’ CaraGen =
(π β OutMeas β¦
{π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
20 | 18, 19 | fvmptg 6951 |
. 2
β’ ((π β OutMeas β§ {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) β (CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
21 | 1, 6, 20 | syl2anc 585 |
1
β’ (π β OutMeas β
(CaraGenβπ) = {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |