Theorem homarcl

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

	Ref	Expression
Hypothesis	homarcl.h	|- H = ( HomA ` C )
Assertion	homarcl	|- ( F e. ( X H Y ) -> C e. Cat )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	|- H = ( HomA ` C )
2		n0i	|- ( F e. ( X H Y ) -> -. ( X H Y ) = (/) )
3		df-homa	|- HomA = ( c e. Cat |-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) |-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
4	3	fvmptndm	|- ( -. C e. Cat -> ( HomA ` C ) = (/) )
5	1 4	eqtrid	|- ( -. C e. Cat -> H = (/) )
6	5	oveqd	|- ( -. C e. Cat -> ( X H Y ) = ( X (/) Y ) )
7		0ov	|- ( X (/) Y ) = (/)
8	6 7	eqtrdi	|- ( -. C e. Cat -> ( X H Y ) = (/) )
9	2 8	nsyl2	|- ( F e. ( X H Y ) -> C e. Cat )