Step | Hyp | Ref
| Expression |
1 | | df-carsg 33599 |
. 2
β’
toCaraSiga = (π
β V β¦ {π β
π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
2 | | simpr 483 |
. . . . . . . 8
β’ ((π β§ π = π) β π = π) |
3 | 2 | dmeqd 5904 |
. . . . . . 7
β’ ((π β§ π = π) β dom π = dom π) |
4 | | carsgval.2 |
. . . . . . . . 9
β’ (π β π:π« πβΆ(0[,]+β)) |
5 | 4 | fdmd 6727 |
. . . . . . . 8
β’ (π β dom π = π« π) |
6 | 5 | adantr 479 |
. . . . . . 7
β’ ((π β§ π = π) β dom π = π« π) |
7 | 3, 6 | eqtrd 2770 |
. . . . . 6
β’ ((π β§ π = π) β dom π = π« π) |
8 | 7 | unieqd 4921 |
. . . . 5
β’ ((π β§ π = π) β βͺ dom
π = βͺ π« π) |
9 | | unipw 5449 |
. . . . 5
β’ βͺ π« π = π |
10 | 8, 9 | eqtrdi 2786 |
. . . 4
β’ ((π β§ π = π) β βͺ dom
π = π) |
11 | 10 | pweqd 4618 |
. . 3
β’ ((π β§ π = π) β π« βͺ dom π = π« π) |
12 | | fveq1 6889 |
. . . . . . 7
β’ (π = π β (πβ(π β© π)) = (πβ(π β© π))) |
13 | | fveq1 6889 |
. . . . . . 7
β’ (π = π β (πβ(π β π)) = (πβ(π β π))) |
14 | 12, 13 | oveq12d 7429 |
. . . . . 6
β’ (π = π β ((πβ(π β© π)) +π (πβ(π β π))) = ((πβ(π β© π)) +π (πβ(π β π)))) |
15 | | fveq1 6889 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
16 | 14, 15 | eqeq12d 2746 |
. . . . 5
β’ (π = π β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
17 | 16 | adantl 480 |
. . . 4
β’ ((π β§ π = π) β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
18 | 11, 17 | raleqbidv 3340 |
. . 3
β’ ((π β§ π = π) β (βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
19 | 11, 18 | rabeqbidv 3447 |
. 2
β’ ((π β§ π = π) β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} = {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
20 | | carsgval.1 |
. . . 4
β’ (π β π β π) |
21 | 20 | pwexd 5376 |
. . 3
β’ (π β π« π β V) |
22 | 4, 21 | fexd 7230 |
. 2
β’ (π β π β V) |
23 | | pwexg 5375 |
. . 3
β’ (π β π β π« π β V) |
24 | | rabexg 5330 |
. . 3
β’
(π« π β
V β {π β
π« π β£
βπ β π«
π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) |
25 | 20, 23, 24 | 3syl 18 |
. 2
β’ (π β {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) |
26 | 1, 19, 22, 25 | fvmptd2 7005 |
1
β’ (π β (toCaraSigaβπ) = {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |