Step | Hyp | Ref
| Expression |
1 | | carsgval.1 |
. . . 4
β’ (π β π β π) |
2 | | carsgval.2 |
. . . 4
β’ (π β π:π« πβΆ(0[,]+β)) |
3 | 1, 2 | carsgval 32943 |
. . 3
β’ (π β (toCaraSigaβπ) = {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)}) |
4 | 3 | eleq2d 2824 |
. 2
β’ (π β (π΄ β (toCaraSigaβπ) β π΄ β {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)})) |
5 | | ineq2 4171 |
. . . . . . . 8
β’ (π = π΄ β (π β© π) = (π β© π΄)) |
6 | 5 | fveq2d 6851 |
. . . . . . 7
β’ (π = π΄ β (πβ(π β© π)) = (πβ(π β© π΄))) |
7 | | difeq2 4081 |
. . . . . . . 8
β’ (π = π΄ β (π β π) = (π β π΄)) |
8 | 7 | fveq2d 6851 |
. . . . . . 7
β’ (π = π΄ β (πβ(π β π)) = (πβ(π β π΄))) |
9 | 6, 8 | oveq12d 7380 |
. . . . . 6
β’ (π = π΄ β ((πβ(π β© π)) +π (πβ(π β π))) = ((πβ(π β© π΄)) +π (πβ(π β π΄)))) |
10 | 9 | eqeq1d 2739 |
. . . . 5
β’ (π = π΄ β (((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β ((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ))) |
11 | 10 | ralbidv 3175 |
. . . 4
β’ (π = π΄ β (βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ) β βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ))) |
12 | 11 | elrab 3650 |
. . 3
β’ (π΄ β {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β (π΄ β π« π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ))) |
13 | | elex 3466 |
. . . . . 6
β’ (π΄ β π« π β π΄ β V) |
14 | 13 | a1i 11 |
. . . . 5
β’ (π β (π΄ β π« π β π΄ β V)) |
15 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π΄ β π) β π β π) |
16 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π΄ β π) β π΄ β π) |
17 | 15, 16 | ssexd 5286 |
. . . . . 6
β’ ((π β§ π΄ β π) β π΄ β V) |
18 | 17 | ex 414 |
. . . . 5
β’ (π β (π΄ β π β π΄ β V)) |
19 | | elpwg 4568 |
. . . . . 6
β’ (π΄ β V β (π΄ β π« π β π΄ β π)) |
20 | 19 | a1i 11 |
. . . . 5
β’ (π β (π΄ β V β (π΄ β π« π β π΄ β π))) |
21 | 14, 18, 20 | pm5.21ndd 381 |
. . . 4
β’ (π β (π΄ β π« π β π΄ β π)) |
22 | 21 | anbi1d 631 |
. . 3
β’ (π β ((π΄ β π« π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)) β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)))) |
23 | 12, 22 | bitrid 283 |
. 2
β’ (π β (π΄ β {π β π« π β£ βπ β π« π((πβ(π β© π)) +π (πβ(π β π))) = (πβπ)} β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)))) |
24 | 4, 23 | bitrd 279 |
1
β’ (π β (π΄ β (toCaraSigaβπ) β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)))) |