homarcl

Description: Reverse closure for an arrow. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Hypothesis	homarcl.h	$⊢ H = {Hom}_{a} (C)$
	Assertion	homarcl	$⊢ F \in (X H Y) \to C \in Cat$

Step	Hyp	Ref	Expression
1		homarcl.h	$⊢ H = {Hom}_{a} (C)$
2		n0i	$⊢ F \in (X H Y) \to \neg X H Y = \emptyset$
3		df-homa	$⊢ {Hom}_{a} = (c \in Cat ⟼ (x \in ({Base}_{c} \times {Base}_{c}) ⟼ \{x\} \times Hom (c) (x)))$
4	3	fvmptndm	$⊢ \neg C \in Cat \to {Hom}_{a} (C) = \emptyset$
5	1 4	eqtrid	$⊢ \neg C \in Cat \to H = \emptyset$
6	5	oveqd	$⊢ \neg C \in Cat \to X H Y = X \emptyset Y$
7		0ov	$⊢ X \emptyset Y = \emptyset$
8	6 7	eqtrdi	$⊢ \neg C \in Cat \to X H Y = \emptyset$
9	2 8	nsyl2	$⊢ F \in (X H Y) \to C \in Cat$

Metamath Proof Explorer