Theorem homarcl2

Description: Reverse closure for the domain and codomain of an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homahom.h	$$⊢H={Hom}_a\left(C\right)$$
	homarcl2.b	$$⊢B={\mathrm{Base}}_C$$
Assertion	homarcl2	$$⊢F\in \left(XHY\right)\to \left(X\in B\wedge Y\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		homahom.h	$$⊢H={Hom}_a\left(C\right)$$
2		homarcl2.b	$$⊢B={\mathrm{Base}}_C$$
3		elfvdm	$$⊢F\in H\left(⟨X,Y⟩\right)\to ⟨X,Y⟩\in \mathrm{dom}H$$
4		df-ov	$$⊢XHY=H\left(⟨X,Y⟩\right)$$
5	3 4	eleq2s	$$⊢F\in \left(XHY\right)\to ⟨X,Y⟩\in \mathrm{dom}H$$
6	1	homarcl	$$⊢F\in \left(XHY\right)\to C\in \mathrm{Cat}$$
7	1 2 6	homaf	$$⊢F\in \left(XHY\right)\to H:B\times B⟶𝒫\left(\left(B\times B\right)\times \mathrm{V}\right)$$
8	7	fdmd	$$⊢F\in \left(XHY\right)\to \mathrm{dom}H=B\times B$$
9	5 8	eleqtrd	$$⊢F\in \left(XHY\right)\to ⟨X,Y⟩\in \left(B\times B\right)$$
10		opelxp	$$⊢⟨X,Y⟩\in \left(B\times B\right)\leftrightarrow \left(X\in B\wedge Y\in B\right)$$
11	9 10	sylib	$$⊢F\in \left(XHY\right)\to \left(X\in B\wedge Y\in B\right)$$