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

Metamath Proof Explorer

Theorem initorcl

Description: Reverse closure for an initial object: If a class has an initial object, the class is a category. (Contributed by AV, 4-Apr-2020)

Ref Expression
Assertion initorcl ⊢ I ∈ InitO ⁡ C → C ∈ Cat

Proof

Step Hyp Ref Expression
1 df-inito ⊢ InitO = c ∈ Cat ⟼ a ∈ Base c | ∀ b ∈ Base c ∃! h h ∈ a Hom ⁡ c b
2 1 mptrcl ⊢ I ∈ InitO ⁡ C → C ∈ Cat