Metamath Proof Explorer


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 )