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 ) )