Metamath Proof Explorer


Theorem isthinc3

Description: A thin category is a category in which, given a pair of objects x and y and any two morphisms f , g from x to y , the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthinc.b B = Base C
isthinc.h H = Hom C
Assertion isthinc3 C ThinCat C Cat x B y B f x H y g x H y f = g

Proof

Step Hyp Ref Expression
1 isthinc.b B = Base C
2 isthinc.h H = Hom C
3 1 2 isthinc C ThinCat C Cat x B y B * f f x H y
4 moel * f f x H y f x H y g x H y f = g
5 4 2ralbii x B y B * f f x H y x B y B f x H y g x H y f = g
6 5 anbi2i C Cat x B y B * f f x H y C Cat x B y B f x H y g x H y f = g
7 3 6 bitri C ThinCat C Cat x B y B f x H y g x H y f = g