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

Metamath Proof Explorer

Theorem thincmo

Description: There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses thincmo.c 
|- ( ph -> C e. ThinCat )
thincmo.x 
|- ( ph -> X e. B )
thincmo.y 
|- ( ph -> Y e. B )
thincmo.b 
|- B = ( Base ` C )
thincmo.h 
|- H = ( Hom ` C )
Assertion thincmo 
|- ( ph -> E* f f e. ( X H Y ) )

Proof

Step Hyp Ref Expression
1 thincmo.c 
 |-  ( ph -> C e. ThinCat )
2 thincmo.x 
 |-  ( ph -> X e. B )
3 thincmo.y 
 |-  ( ph -> Y e. B )
4 thincmo.b 
 |-  B = ( Base ` C )
5 thincmo.h 
 |-  H = ( Hom ` C )
6 2 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> X e. B )
7 3 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> Y e. B )
8 simprl 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> f e. ( X H Y ) )
9 simprr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> g e. ( X H Y ) )
10 1 adantr 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> C e. ThinCat )
11 6 7 8 9 4 5 10 thincmo2 
 |-  ( ( ph /\ ( f e. ( X H Y ) /\ g e. ( X H Y ) ) ) -> f = g )
12 11 ex 
 |-  ( ph -> ( ( f e. ( X H Y ) /\ g e. ( X H Y ) ) -> f = g ) )
13 12 alrimivv 
 |-  ( ph -> A. f A. g ( ( f e. ( X H Y ) /\ g e. ( X H Y ) ) -> f = g ) )
14 eleq1w 
 |-  ( f = g -> ( f e. ( X H Y ) <-> g e. ( X H Y ) ) )
15 14 mo4 
 |-  ( E* f f e. ( X H Y ) <-> A. f A. g ( ( f e. ( X H Y ) /\ g e. ( X H Y ) ) -> f = g ) )
16 13 15 sylibr 
 |-  ( ph -> E* f f e. ( X H Y ) )