Theorem relxpchom

Description: A hom-set in the binary product of categories is a relation. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	relxpchom.t	$$⊢T=C{\times }_{c}D$$
	relxpchom.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
Assertion	relxpchom	$$⊢\mathrm{Rel}\left(XKY\right)$$

Proof

Step	Hyp	Ref	Expression
1		relxpchom.t	$$⊢T=C{\times }_{c}D$$
2		relxpchom.k	$$⊢K=\mathrm{Hom}\left(T\right)$$
3		xpss	$$⊢\left(1^{st}\left(u\right)\mathrm{Hom}\left(C\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(D\right)2^{nd}\left(v\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
4	3	rgen2w	$$⊢\forall u\in {\mathrm{Base}}_T\forall v\in {\mathrm{Base}}_T\left(1^{st}\left(u\right)\mathrm{Hom}\left(C\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(D\right)2^{nd}\left(v\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
5		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
6		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
7		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
8	1 5 6 7 2	xpchomfval	$$⊢K=\left(u\in {\mathrm{Base}}_T,v\in {\mathrm{Base}}_T⟼\left(1^{st}\left(u\right)\mathrm{Hom}\left(C\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(D\right)2^{nd}\left(v\right)\right)\right)$$
9	8	ovmptss	$$⊢\forall u\in {\mathrm{Base}}_T\forall v\in {\mathrm{Base}}_T\left(1^{st}\left(u\right)\mathrm{Hom}\left(C\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(D\right)2^{nd}\left(v\right)\right)\subseteq \mathrm{V}\times \mathrm{V}\to XKY\subseteq \mathrm{V}\times \mathrm{V}$$
10	4 9	ax-mp	$$⊢XKY\subseteq \mathrm{V}\times \mathrm{V}$$
11		df-rel	$$⊢\mathrm{Rel}\left(XKY\right)\leftrightarrow XKY\subseteq \mathrm{V}\times \mathrm{V}$$
12	10 11	mpbir	$$⊢\mathrm{Rel}\left(XKY\right)$$