Metamath Proof Explorer


Theorem 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 X H Y C Cat

Proof

Step Hyp Ref Expression
1 homarcl.h H = Hom a C
2 n0i F X H Y ¬ X H Y =
3 df-homa Hom a = c Cat x Base c × Base c x × Hom c x
4 3 fvmptndm ¬ C Cat Hom a C =
5 1 4 eqtrid ¬ C Cat H =
6 5 oveqd ¬ C Cat X H Y = X Y
7 0ov X Y =
8 6 7 eqtrdi ¬ C Cat X H Y =
9 2 8 nsyl2 F X H Y C Cat