This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thincc

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

Ref Expression
Assertion thincc ⊢ C ∈ ThinCat → C ∈ Cat

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base C = Base C
2 eqid ⊢ Hom ⁡ C = Hom ⁡ C
3 1 2 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ Base C ∀ y ∈ Base C ∃* f f ∈ x Hom ⁡ C y
4 3 simplbi ⊢ C ∈ ThinCat → C ∈ Cat