Step | Hyp | Ref
| Expression |
1 | | arwval.a |
. 2
β’ π΄ = (ArrowβπΆ) |
2 | | fveq2 6892 |
. . . . . . 7
β’ (π = πΆ β (Homaβπ) =
(HomaβπΆ)) |
3 | | arwval.h |
. . . . . . 7
β’ π» =
(HomaβπΆ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . 6
β’ (π = πΆ β (Homaβπ) = π») |
5 | 4 | rneqd 5938 |
. . . . 5
β’ (π = πΆ β ran
(Homaβπ) = ran π») |
6 | 5 | unieqd 4923 |
. . . 4
β’ (π = πΆ β βͺ ran
(Homaβπ) = βͺ ran π») |
7 | | df-arw 17977 |
. . . 4
β’ Arrow =
(π β Cat β¦ βͺ ran (Homaβπ)) |
8 | 3 | fvexi 6906 |
. . . . . 6
β’ π» β V |
9 | 8 | rnex 7903 |
. . . . 5
β’ ran π» β V |
10 | 9 | uniex 7731 |
. . . 4
β’ βͺ ran π» β V |
11 | 6, 7, 10 | fvmpt 6999 |
. . 3
β’ (πΆ β Cat β
(ArrowβπΆ) = βͺ ran π») |
12 | 7 | fvmptndm 7029 |
. . . 4
β’ (Β¬
πΆ β Cat β
(ArrowβπΆ) =
β
) |
13 | | df-homa 17976 |
. . . . . . . . . 10
β’
Homa = (π β Cat β¦ (π₯ β ((Baseβπ) Γ (Baseβπ)) β¦ ({π₯} Γ ((Hom βπ)βπ₯)))) |
14 | 13 | fvmptndm 7029 |
. . . . . . . . 9
β’ (Β¬
πΆ β Cat β
(HomaβπΆ) = β
) |
15 | 3, 14 | eqtrid 2785 |
. . . . . . . 8
β’ (Β¬
πΆ β Cat β π» = β
) |
16 | 15 | rneqd 5938 |
. . . . . . 7
β’ (Β¬
πΆ β Cat β ran
π» = ran
β
) |
17 | | rn0 5926 |
. . . . . . 7
β’ ran
β
= β
|
18 | 16, 17 | eqtrdi 2789 |
. . . . . 6
β’ (Β¬
πΆ β Cat β ran
π» =
β
) |
19 | 18 | unieqd 4923 |
. . . . 5
β’ (Β¬
πΆ β Cat β βͺ ran π» = βͺ
β
) |
20 | | uni0 4940 |
. . . . 5
β’ βͺ β
= β
|
21 | 19, 20 | eqtrdi 2789 |
. . . 4
β’ (Β¬
πΆ β Cat β βͺ ran π» = β
) |
22 | 12, 21 | eqtr4d 2776 |
. . 3
β’ (Β¬
πΆ β Cat β
(ArrowβπΆ) = βͺ ran π») |
23 | 11, 22 | pm2.61i 182 |
. 2
β’
(ArrowβπΆ) =
βͺ ran π» |
24 | 1, 23 | eqtri 2761 |
1
β’ π΄ = βͺ
ran π» |