Step | Hyp | Ref
| Expression |
1 | | df-carsg 33600 |
. 2
β’
toCaraSiga = (π
β V β¦ {π β
π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
2 | | simpr 484 |
. . . . . . . 8
β’ ((π β§ π = π) β π = π) |
3 | 2 | dmeqd 5905 |
. . . . . . 7
β’ ((π β§ π = π) β dom π = dom π) |
4 | | carsgval.2 |
. . . . . . . . 9
β’ (π β π:π« πβΆ(0[,]+β)) |
5 | 4 | fdmd 6728 |
. . . . . . . 8
β’ (π β dom π = π« π) |
6 | 5 | adantr 480 |
. . . . . . 7
β’ ((π β§ π = π) β dom π = π« π) |
7 | 3, 6 | eqtrd 2771 |
. . . . . 6
β’ ((π β§ π = π) β dom π = π« π) |
8 | 7 | unieqd 4922 |
. . . . 5
β’ ((π β§ π = π) β βͺ dom
π = βͺ π« π) |
9 | | unipw 5450 |
. . . . 5
β’ βͺ π« π = π |
10 | 8, 9 | eqtrdi 2787 |
. . . 4
β’ ((π β§ π = π) β βͺ dom
π = π) |
11 | 10 | pweqd 4619 |
. . 3
β’ ((π β§ π = π) β π« βͺ dom π = π« π) |
12 | | fveq1 6890 |
. . . . . . 7
β’ (π = π β (πβ(π β© π)) = (πβ(π β© π))) |
13 | | fveq1 6890 |
. . . . . . 7
β’ (π = π β (πβ(π β π)) = (πβ(π β π))) |
14 | 12, 13 | oveq12d 7430 |
. . . . . 6
β’ (π = π β ((πβ(π β© π)) +π (πβ(π β π))) = ((πβ(π β© π)) +π (πβ(π β π)))) |
15 | | fveq1 6890 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
16 | 14, 15 | eqeq12d 2747 |
. . . . 5
β’ (π = π β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
17 | 16 | adantl 481 |
. . . 4
β’ ((π β§ π = π) β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
18 | 11, 17 | raleqbidv 3341 |
. . 3
β’ ((π β§ π = π) β (βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ))) |
19 | 11, 18 | rabeqbidv 3448 |
. 2
β’ ((π β§ π = π) β {π β π« βͺ dom π β£ βπ β π« βͺ dom π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} = {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
20 | | carsgval.1 |
. . . 4
β’ (π β π β π) |
21 | 20 | pwexd 5377 |
. . 3
β’ (π β π« π β V) |
22 | 4, 21 | fexd 7231 |
. 2
β’ (π β π β V) |
23 | | pwexg 5376 |
. . 3
β’ (π β π β π« π β V) |
24 | | rabexg 5331 |
. . 3
β’
(π« π β
V β {π β
π« π β£
βπ β π«
π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) |
25 | 20, 23, 24 | 3syl 18 |
. 2
β’ (π β {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β V) |
26 | 1, 19, 22, 25 | fvmptd2 7006 |
1
β’ (π β (toCaraSigaβπ) = {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |