Theorem homarcl

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

	Ref	Expression
Hypothesis	homarcl.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
Assertion	homarcl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	⊢ 𝐻 = ( Homa ‘ 𝐶 )
2		n0i	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )
3		df-homa	⊢ Homa = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) ↦ ( { 𝑥 } × ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ) ) )
4	3	fvmptndm	⊢ ( ¬ 𝐶 ∈ Cat → ( Homa ‘ 𝐶 ) = ∅ )
5	1 4	eqtrid	⊢ ( ¬ 𝐶 ∈ Cat → 𝐻 = ∅ )
6	5	oveqd	⊢ ( ¬ 𝐶 ∈ Cat → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ∅ 𝑌 ) )
7		0ov	⊢ ( 𝑋 ∅ 𝑌 ) = ∅
8	6 7	eqtrdi	⊢ ( ¬ 𝐶 ∈ Cat → ( 𝑋 𝐻 𝑌 ) = ∅ )
9	2 8	nsyl2	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → 𝐶 ∈ Cat )