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

Metamath Proof Explorer

Theorem thinchom

Description: A non-empty hom-set of a thin category is given by its element. (Contributed by Zhi Wang, 20-Oct-2025)

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

Proof

Step Hyp Ref Expression
1 thinchom.x 
 |-  ( ph -> X e. B )
2 thinchom.y 
 |-  ( ph -> Y e. B )
3 thinchom.f 
 |-  ( ph -> F e. ( X H Y ) )
4 thinchom.b 
 |-  B = ( Base ` C )
5 thinchom.h 
 |-  H = ( Hom ` C )
6 thinchom.c 
 |-  ( ph -> C e. ThinCat )
7 1 adantr 
 |-  ( ( ph /\ g e. ( X H Y ) ) -> X e. B )
8 2 adantr 
 |-  ( ( ph /\ g e. ( X H Y ) ) -> Y e. B )
9 simpr 
 |-  ( ( ph /\ g e. ( X H Y ) ) -> g e. ( X H Y ) )
10 3 adantr 
 |-  ( ( ph /\ g e. ( X H Y ) ) -> F e. ( X H Y ) )
11 6 adantr 
 |-  ( ( ph /\ g e. ( X H Y ) ) -> C e. ThinCat )
12 7 8 9 10 4 5 11 thincmo2 
 |-  ( ( ph /\ g e. ( X H Y ) ) -> g = F )
13 12 3 eqsnd 
 |-  ( ph -> ( X H Y ) = { F } )