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=\mathrm{SetCat}\left(U\right)$$
	setcbas.u	$$⊢\phi \to U\in V$$
	setchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	setchom.x	$$⊢\phi \to X\in U$$
	setchom.y	$$⊢\phi \to Y\in U$$
Assertion	setchom	$$⊢\phi \to XHY=Y^X$$

Proof

Step	Hyp	Ref	Expression
1		setcbas.c	$$⊢C=\mathrm{SetCat}\left(U\right)$$
2		setcbas.u	$$⊢\phi \to U\in V$$
3		setchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		setchom.x	$$⊢\phi \to X\in U$$
5		setchom.y	$$⊢\phi \to Y\in U$$
6	1 2 3	setchomfval	$$⊢\phi \to H=\left(x\in U,y\in U⟼y^x\right)$$
7		simprr	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to y=Y$$
8		simprl	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to x=X$$
9	7 8	oveq12d	$$⊢\left(\phi \wedge \left(x=X\wedge y=Y\right)\right)\to y^x=Y^X$$
10		ovexd	$$⊢\phi \to Y^X\in \mathrm{V}$$
11	6 9 4 5 10	ovmpod	$$⊢\phi \to XHY=Y^X$$