Theorem istermc3

Description: The predicate "is a terminal category". A terminal category is a thin category whose base set is equinumerous to 1o . Consider en1b , map1 , and euen1b . (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypothesis	istermc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	istermc3	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ 𝐵 ≈ 1o ) )

Proof

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