Theorem istermc2

Description: The predicate "is a terminal category". A terminal category is a thin category with exactly one object. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypothesis	istermc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	istermc2	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		istermc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2	1	istermc	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 𝐵 = { 𝑥 } ) )
3		eusn	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐵 ↔ ∃ 𝑥 𝐵 = { 𝑥 } )
4	3	anbi2i	⊢ ( ( 𝐶 ∈ ThinCat ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 𝐵 = { 𝑥 } ) )
5	2 4	bitr4i	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃! 𝑥 𝑥 ∈ 𝐵 ) )