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

Metamath Proof Explorer

Theorem termchomn0

Description: All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses termcbas.c 
|- ( ph -> C e. TermCat )
termcbas.b 
|- B = ( Base ` C )
termcbasmo.x 
|- ( ph -> X e. B )
termcbasmo.y 
|- ( ph -> Y e. B )
termcid.h 
|- H = ( Hom ` C )
Assertion termchomn0 
|- ( ph -> -. ( X H Y ) = (/) )

Proof

Step Hyp Ref Expression
1 termcbas.c 
 |-  ( ph -> C e. TermCat )
2 termcbas.b 
 |-  B = ( Base ` C )
3 termcbasmo.x 
 |-  ( ph -> X e. B )
4 termcbasmo.y 
 |-  ( ph -> Y e. B )
5 termcid.h 
 |-  H = ( Hom ` C )
6 eqid 
 |-  ( Id ` C ) = ( Id ` C )
7 1 termccd 
 |-  ( ph -> C e. Cat )
8 2 5 6 7 3 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X H X ) )
9 1 2 3 4 termcbasmo 
 |-  ( ph -> X = Y )
10 9 oveq2d 
 |-  ( ph -> ( X H X ) = ( X H Y ) )
11 8 10 eleqtrd 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X H Y ) )
12 n0i 
 |-  ( ( ( Id ` C ) ` X ) e. ( X H Y ) -> -. ( X H Y ) = (/) )
13 11 12 syl 
 |-  ( ph -> -. ( X H Y ) = (/) )