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