Theorem xpchom

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpchomfval.t	$$⊢T=C{\times }_{c}D$$
	xpchomfval.y	$$⊢B={\mathrm{Base}}_T$$
	xpchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	xpchomfval.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	xpchomfval.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
	xpchom.x	$$⊢\phi \to X\in B$$
	xpchom.y	$$⊢\phi \to Y\in B$$
Assertion	xpchom	$$⊢\phi \to XKY=\left(1^{st}\left(X\right)H{1}^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpchomfval.t	$$⊢T=C{\times }_{c}D$$
2		xpchomfval.y	$$⊢B={\mathrm{Base}}_T$$
3		xpchomfval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		xpchomfval.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
5		xpchomfval.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
6		xpchom.x	$$⊢\phi \to X\in B$$
7		xpchom.y	$$⊢\phi \to Y\in B$$
8		simpl	$$⊢\left(u=X\wedge v=Y\right)\to u=X$$
9	8	fveq2d	$$⊢\left(u=X\wedge v=Y\right)\to 1^{st}\left(u\right)=1^{st}\left(X\right)$$
10		simpr	$$⊢\left(u=X\wedge v=Y\right)\to v=Y$$
11	10	fveq2d	$$⊢\left(u=X\wedge v=Y\right)\to 1^{st}\left(v\right)=1^{st}\left(Y\right)$$
12	9 11	oveq12d	$$⊢\left(u=X\wedge v=Y\right)\to 1^{st}\left(u\right)H{1}^{st}\left(v\right)=1^{st}\left(X\right)H{1}^{st}\left(Y\right)$$
13	8	fveq2d	$$⊢\left(u=X\wedge v=Y\right)\to 2^{nd}\left(u\right)=2^{nd}\left(X\right)$$
14	10	fveq2d	$$⊢\left(u=X\wedge v=Y\right)\to 2^{nd}\left(v\right)=2^{nd}\left(Y\right)$$
15	13 14	oveq12d	$$⊢\left(u=X\wedge v=Y\right)\to 2^{nd}\left(u\right)J{2}^{nd}\left(v\right)=2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)$$
16	12 15	xpeq12d	$$⊢\left(u=X\wedge v=Y\right)\to \left(1^{st}\left(u\right)H{1}^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)J{2}^{nd}\left(v\right)\right)=\left(1^{st}\left(X\right)H{1}^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)\right)$$
17	1 2 3 4 5	xpchomfval	$$⊢K=\left(u\in B,v\in B⟼\left(1^{st}\left(u\right)H{1}^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)J{2}^{nd}\left(v\right)\right)\right)$$
18		ovex	$$⊢1^{st}\left(X\right)H{1}^{st}\left(Y\right)\in \mathrm{V}$$
19		ovex	$$⊢2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)\in \mathrm{V}$$
20	18 19	xpex	$$⊢\left(1^{st}\left(X\right)H{1}^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)\right)\in \mathrm{V}$$
21	16 17 20	ovmpoa	$$⊢\left(X\in B\wedge Y\in B\right)\to XKY=\left(1^{st}\left(X\right)H{1}^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)\right)$$
22	6 7 21	syl2anc	$$⊢\phi \to XKY=\left(1^{st}\left(X\right)H{1}^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)J{2}^{nd}\left(Y\right)\right)$$