This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setchom

Description: Set of arrows of the category of sets (in a universe). (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcbas.c 
|- C = ( SetCat ` U )
setcbas.u 
|- ( ph -> U e. V )
setchomfval.h 
|- H = ( Hom ` C )
setchom.x 
|- ( ph -> X e. U )
setchom.y 
|- ( ph -> Y e. U )
Assertion setchom 
|- ( ph -> ( X H Y ) = ( Y ^m X ) )

Proof

Step Hyp Ref Expression
1 setcbas.c 
 |-  C = ( SetCat ` U )
2 setcbas.u 
 |-  ( ph -> U e. V )
3 setchomfval.h 
 |-  H = ( Hom ` C )
4 setchom.x 
 |-  ( ph -> X e. U )
5 setchom.y 
 |-  ( ph -> Y e. U )
6 1 2 3 setchomfval 
 |-  ( ph -> H = ( x e. U , y e. U |-> ( y ^m x ) ) )
7 simprr 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y )
8 simprl 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X )
9 7 8 oveq12d 
 |-  ( ( ph /\ ( x = X /\ y = Y ) ) -> ( y ^m x ) = ( Y ^m X ) )
10 ovexd 
 |-  ( ph -> ( Y ^m X ) e. _V )
11 6 9 4 5 10 ovmpod 
 |-  ( ph -> ( X H Y ) = ( Y ^m X ) )