Description: Set of arrows of the category of categories (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | catcbas.c | |- C = ( CatCat ` U ) |
|
catcbas.b | |- B = ( Base ` C ) |
||
catcbas.u | |- ( ph -> U e. V ) |
||
catchomfval.h | |- H = ( Hom ` C ) |
||
catchom.x | |- ( ph -> X e. B ) |
||
catchom.y | |- ( ph -> Y e. B ) |
||
Assertion | catchom | |- ( ph -> ( X H Y ) = ( X Func Y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | catcbas.c | |- C = ( CatCat ` U ) |
|
2 | catcbas.b | |- B = ( Base ` C ) |
|
3 | catcbas.u | |- ( ph -> U e. V ) |
|
4 | catchomfval.h | |- H = ( Hom ` C ) |
|
5 | catchom.x | |- ( ph -> X e. B ) |
|
6 | catchom.y | |- ( ph -> Y e. B ) |
|
7 | 1 2 3 4 | catchomfval | |- ( ph -> H = ( x e. B , y e. B |-> ( x Func y ) ) ) |
8 | oveq12 | |- ( ( x = X /\ y = Y ) -> ( x Func y ) = ( X Func Y ) ) |
|
9 | 8 | adantl | |- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x Func y ) = ( X Func Y ) ) |
10 | ovexd | |- ( ph -> ( X Func Y ) e. _V ) |
|
11 | 7 9 5 6 10 | ovmpod | |- ( ph -> ( X H Y ) = ( X Func Y ) ) |