This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( 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 e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )
4 moel 
 |-  ( E* f f e. ( x H y ) <-> A. f e. ( x H y ) A. g e. ( x H y ) f = g )
5 4 2ralbii 
 |-  ( A. x e. B A. y e. B E* f f e. ( x H y ) <-> A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g )
6 5 anbi2i 
 |-  ( ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) )
7 3 6 bitri 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) )