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

Metamath Proof Explorer

Theorem thincmo2

Description: Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd2lem1.1 
|- ( ph -> X e. B )
isthincd2lem1.2 
|- ( ph -> Y e. B )
isthincd2lem1.3 
|- ( ph -> F e. ( X H Y ) )
isthincd2lem1.4 
|- ( ph -> G e. ( X H Y ) )
thincmo2.b 
|- B = ( Base ` C )
thincmo2.h 
|- H = ( Hom ` C )
thincmo2.c 
|- ( ph -> C e. ThinCat )
Assertion thincmo2 
|- ( ph -> F = G )

Proof

Step Hyp Ref Expression
1 isthincd2lem1.1 
 |-  ( ph -> X e. B )
2 isthincd2lem1.2 
 |-  ( ph -> Y e. B )
3 isthincd2lem1.3 
 |-  ( ph -> F e. ( X H Y ) )
4 isthincd2lem1.4 
 |-  ( ph -> G e. ( X H Y ) )
5 thincmo2.b 
 |-  B = ( Base ` C )
6 thincmo2.h 
 |-  H = ( Hom ` C )
7 thincmo2.c 
 |-  ( ph -> C e. ThinCat )
8 5 6 isthinc 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )
9 8 simprbi 
 |-  ( C e. ThinCat -> A. x e. B A. y e. B E* f f e. ( x H y ) )
10 7 9 syl 
 |-  ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
11 1 2 3 4 10 isthincd2lem1 
 |-  ( ph -> F = G )