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

Metamath Proof Explorer

Theorem termchom

Description: The hom-set of a terminal category is a singleton of the identity morphism. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses termchom.c 
|- ( ph -> C e. TermCat )
termchom.b 
|- B = ( Base ` C )
termchom.x 
|- ( ph -> X e. B )
termchom.y 
|- ( ph -> Y e. B )
termchom.h 
|- H = ( Hom ` C )
termchom.i 
|- .1. = ( Id ` C )
Assertion termchom 
|- ( ph -> ( X H Y ) = { ( .1. ` X ) } )

Proof

Step Hyp Ref Expression
1 termchom.c 
 |-  ( ph -> C e. TermCat )
2 termchom.b 
 |-  B = ( Base ` C )
3 termchom.x 
 |-  ( ph -> X e. B )
4 termchom.y 
 |-  ( ph -> Y e. B )
5 termchom.h 
 |-  H = ( Hom ` C )
6 termchom.i 
 |-  .1. = ( Id ` C )
7 1 2 3 4 5 termchomn0 
 |-  ( ph -> -. ( X H Y ) = (/) )
8 neq0 
 |-  ( -. ( X H Y ) = (/) <-> E. f f e. ( X H Y ) )
9 7 8 sylib 
 |-  ( ph -> E. f f e. ( X H Y ) )
10 3 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> X e. B )
11 4 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> Y e. B )
12 simpr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> f e. ( X H Y ) )
13 1 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> C e. TermCat )
14 13 termcthind 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> C e. ThinCat )
15 10 11 12 2 5 14 thinchom 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( X H Y ) = { f } )
16 13 2 10 11 5 12 6 termcid 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> f = ( .1. ` X ) )
17 16 sneqd 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> { f } = { ( .1. ` X ) } )
18 15 17 eqtrd 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( X H Y ) = { ( .1. ` X ) } )
19 9 18 exlimddv 
 |-  ( ph -> ( X H Y ) = { ( .1. ` X ) } )