Theorem homarel

Description: An arrow is an ordered pair. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypothesis	homahom.h	$$⊢H={Hom}_a\left(C\right)$$
Assertion	homarel	$$⊢\mathrm{Rel}\left(XHY\right)$$

Proof

Step	Hyp	Ref	Expression
1		homahom.h	$$⊢H={Hom}_a\left(C\right)$$
2		xpss	$$⊢\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\times \mathrm{V}\subseteq \mathrm{V}\times \mathrm{V}$$
3		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
4	1	homarcl	$$⊢f\in \left(XHY\right)\to C\in \mathrm{Cat}$$
5	1 3 4	homaf	$$⊢f\in \left(XHY\right)\to H:{\mathrm{Base}}_C\times {\mathrm{Base}}_C⟶𝒫\left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\times \mathrm{V}\right)$$
6	1 3	homarcl2	$$⊢f\in \left(XHY\right)\to \left(X\in {\mathrm{Base}}_C\wedge Y\in {\mathrm{Base}}_C\right)$$
7	6	simpld	$$⊢f\in \left(XHY\right)\to X\in {\mathrm{Base}}_C$$
8	6	simprd	$$⊢f\in \left(XHY\right)\to Y\in {\mathrm{Base}}_C$$
9	5 7 8	fovrnd	$$⊢f\in \left(XHY\right)\to XHY\in 𝒫\left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\times \mathrm{V}\right)$$
10		elelpwi	$$⊢\left(f\in \left(XHY\right)\wedge XHY\in 𝒫\left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\times \mathrm{V}\right)\right)\to f\in \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\times \mathrm{V}\right)$$
11	9 10	mpdan	$$⊢f\in \left(XHY\right)\to f\in \left(\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\times \mathrm{V}\right)$$
12	2 11	sselid	$$⊢f\in \left(XHY\right)\to f\in \left(\mathrm{V}\times \mathrm{V}\right)$$
13	12	ssriv	$$⊢XHY\subseteq \mathrm{V}\times \mathrm{V}$$
14		df-rel	$$⊢\mathrm{Rel}\left(XHY\right)\leftrightarrow XHY\subseteq \mathrm{V}\times \mathrm{V}$$
15	13 14	mpbir	$$⊢\mathrm{Rel}\left(XHY\right)$$