Theorem istermc

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

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

Proof

Step	Hyp	Ref	Expression
1		istermc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		fveqeq2	⊢ ( 𝑐 = 𝐶 → ( ( Base ‘ 𝑐 ) = { 𝑥 } ↔ ( Base ‘ 𝐶 ) = { 𝑥 } ) )
3	2	exbidv	⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) )
4	1	eqeq1i	⊢ ( 𝐵 = { 𝑥 } ↔ ( Base ‘ 𝐶 ) = { 𝑥 } )
5	4	exbii	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } )
6	3 5	bitr4di	⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
7		df-termc	⊢ TermCat = { 𝑐 ∈ ThinCat ∣ ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } }
8	6 7	elrab2	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 𝐵 = { 𝑥 } ) )