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	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
		termcpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
		termcpropd.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
		termcpropd.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
	Assertion	termcpropd	⊢ ( 𝜑 → ( 𝐶 ∈ TermCat ↔ 𝐷 ∈ TermCat ) )

Proof

Step	Hyp	Ref	Expression
1		termcpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
2		termcpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
3		termcpropd.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		termcpropd.4	⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
5	1 2 3 4	thincpropd	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ↔ 𝐷 ∈ ThinCat ) )
6	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
7	6	eqeq1d	⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) = { 𝑥 } ↔ ( Base ‘ 𝐷 ) = { 𝑥 } ) )
8	7	exbidv	⊢ ( 𝜑 → ( ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐷 ) = { 𝑥 } ) )
9	5 8	anbi12d	⊢ ( 𝜑 → ( ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) ↔ ( 𝐷 ∈ ThinCat ∧ ∃ 𝑥 ( Base ‘ 𝐷 ) = { 𝑥 } ) ) )
10		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11	10	istermc	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) )
12		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
13	12	istermc	⊢ ( 𝐷 ∈ TermCat ↔ ( 𝐷 ∈ ThinCat ∧ ∃ 𝑥 ( Base ‘ 𝐷 ) = { 𝑥 } ) )
14	9 11 13	3bitr4g	⊢ ( 𝜑 → ( 𝐶 ∈ TermCat ↔ 𝐷 ∈ TermCat ) )