homarcl2

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

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

Metamath Proof Explorer