Metamath Proof Explorer


Theorem catchom

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 ) )

Proof

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 ) )