Theorem thincc

Description: A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Assertion	thincc	⊢ ( 𝐶 ∈ ThinCat → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
2		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
3	1 2	isthinc	⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∃* 𝑓 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
4	3	simplbi	⊢ ( 𝐶 ∈ ThinCat → 𝐶 ∈ Cat )