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	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	termcpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	termcpropd.3	$$⊢\phi \to C\in V$$
	termcpropd.4	$$⊢\phi \to D\in W$$
Assertion	termcpropd	Could not format assertion : No typesetting found for |- ( ph -> ( C e. TermCat <-> D e. TermCat ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		termcpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2		termcpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
3		termcpropd.3	$$⊢\phi \to C\in V$$
4		termcpropd.4	$$⊢\phi \to D\in W$$
5	1 2 3 4	thincpropd	$$⊢\phi \to \left(C\in \mathrm{ThinCat}\leftrightarrow D\in \mathrm{ThinCat}\right)$$
6	1	homfeqbas	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$
7	6	eqeq1d	$$⊢\phi \to \left({\mathrm{Base}}_C=\left\{x\right\}\leftrightarrow {\mathrm{Base}}_D=\left\{x\right\}\right)$$
8	7	exbidv	$$⊢\phi \to \left(\exists x{\mathrm{Base}}_C=\left\{x\right\}\leftrightarrow \exists x{\mathrm{Base}}_D=\left\{x\right\}\right)$$
9	5 8	anbi12d	$$⊢\phi \to \left(\left(C\in \mathrm{ThinCat}\wedge \exists x{\mathrm{Base}}_C=\left\{x\right\}\right)\leftrightarrow \left(D\in \mathrm{ThinCat}\wedge \exists x{\mathrm{Base}}_D=\left\{x\right\}\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
11	10	istermc	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) ) with typecode |-
12		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
13	12	istermc	Could not format ( D e. TermCat <-> ( D e. ThinCat /\ E. x ( Base ` D ) = { x } ) ) : No typesetting found for |- ( D e. TermCat <-> ( D e. ThinCat /\ E. x ( Base ` D ) = { x } ) ) with typecode |-
14	9 11 13	3bitr4g	Could not format ( ph -> ( C e. TermCat <-> D e. TermCat ) ) : No typesetting found for |- ( ph -> ( C e. TermCat <-> D e. TermCat ) ) with typecode |-