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

Metamath Proof Explorer

Theorem termcpropd

Description: Two structures with the same base, hom-sets and composition operation are either both terminal categories or neither. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses termcpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
termcpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
termcpropd.3 
|- ( ph -> C e. V )
termcpropd.4 
|- ( ph -> D e. W )
Assertion termcpropd 
|- ( ph -> ( C e. TermCat <-> D e. TermCat ) )

Proof

Step Hyp Ref Expression
1 termcpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 termcpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 termcpropd.3 
 |-  ( ph -> C e. V )
4 termcpropd.4 
 |-  ( ph -> D e. W )
5 1 2 3 4 thincpropd 
 |-  ( ph -> ( C e. ThinCat <-> D e. ThinCat ) )
6 1 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
7 6 eqeq1d 
 |-  ( ph -> ( ( Base ` C ) = { x } <-> ( Base ` D ) = { x } ) )
8 7 exbidv 
 |-  ( ph -> ( E. x ( Base ` C ) = { x } <-> E. x ( Base ` D ) = { x } ) )
9 5 8 anbi12d 
 |-  ( ph -> ( ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) <-> ( D e. ThinCat /\ E. x ( Base ` D ) = { x } ) ) )
10 eqid 
 |-  ( Base ` C ) = ( Base ` C )
11 10 istermc 
 |-  ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) )
12 eqid 
 |-  ( Base ` D ) = ( Base ` D )
13 12 istermc 
 |-  ( D e. TermCat <-> ( D e. ThinCat /\ E. x ( Base ` D ) = { x } ) )
14 9 11 13 3bitr4g 
 |-  ( ph -> ( C e. TermCat <-> D e. TermCat ) )