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

Metamath Proof Explorer

Theorem thincmon

Description: In a thin category, all morphisms are monomorphisms. Example 7.33(9) of Adamek p. 110. The converse does not hold. See grptcmon . (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincid.c 
|- ( ph -> C e. ThinCat )
thincid.b 
|- B = ( Base ` C )
thincid.h 
|- H = ( Hom ` C )
thincid.x 
|- ( ph -> X e. B )
thincmon.y 
|- ( ph -> Y e. B )
thincmon.m 
|- M = ( Mono ` C )
Assertion thincmon 
|- ( ph -> ( X M Y ) = ( X H Y ) )

Proof

Step Hyp Ref Expression
1 thincid.c 
 |-  ( ph -> C e. ThinCat )
2 thincid.b 
 |-  B = ( Base ` C )
3 thincid.h 
 |-  H = ( Hom ` C )
4 thincid.x 
 |-  ( ph -> X e. B )
5 thincmon.y 
 |-  ( ph -> Y e. B )
6 thincmon.m 
 |-  M = ( Mono ` C )
7 simpr1 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> z e. B )
8 4 adantr 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> X e. B )
9 simpr2 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> g e. ( z H X ) )
10 simpr3 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> h e. ( z H X ) )
11 1 adantr 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> C e. ThinCat )
12 7 8 9 10 2 3 11 thincmo2 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> g = h )
13 12 a1d 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> ( ( f ( <. z , X >. ( comp ` C ) Y ) g ) = ( f ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
14 13 ralrimivvva 
 |-  ( ph -> A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( f ( <. z , X >. ( comp ` C ) Y ) g ) = ( f ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
15 eqid 
 |-  ( comp ` C ) = ( comp ` C )
16 1 thinccd 
 |-  ( ph -> C e. Cat )
17 2 3 15 6 16 4 5 ismon2 
 |-  ( ph -> ( f e. ( X M Y ) <-> ( f e. ( X H Y ) /\ A. z e. B A. g e. ( z H X ) A. h e. ( z H X ) ( ( f ( <. z , X >. ( comp ` C ) Y ) g ) = ( f ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) ) ) )
18 14 17 mpbiran2d 
 |-  ( ph -> ( f e. ( X M Y ) <-> f e. ( X H Y ) ) )
19 18 eqrdv 
 |-  ( ph -> ( X M Y ) = ( X H Y ) )