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

Metamath Proof Explorer

Theorem thincmod

Description: At most one morphism in each hom-set (deduction form). (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 )
thincn0eu.b 
|- ( ph -> B = ( Base ` C ) )
thincn0eu.h 
|- ( ph -> H = ( Hom ` C ) )
Assertion thincmod 
|- ( 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 thincn0eu.b 
 |-  ( ph -> B = ( Base ` C ) )
5 thincn0eu.h 
 |-  ( ph -> H = ( Hom ` C ) )
6 2 4 eleqtrd 
 |-  ( ph -> X e. ( Base ` C ) )
7 3 4 eleqtrd 
 |-  ( ph -> Y e. ( Base ` C ) )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 1 6 7 8 9 thincmo 
 |-  ( ph -> E* f f e. ( X ( Hom ` C ) Y ) )
11 5 oveqd 
 |-  ( ph -> ( X H Y ) = ( X ( Hom ` C ) Y ) )
12 11 eleq2d 
 |-  ( ph -> ( f e. ( X H Y ) <-> f e. ( X ( Hom ` C ) Y ) ) )
13 12 mobidv 
 |-  ( ph -> ( E* f f e. ( X H Y ) <-> E* f f e. ( X ( Hom ` C ) Y ) ) )
14 10 13 mpbird 
 |-  ( ph -> E* f f e. ( X H Y ) )