Metamath Proof Explorer

Theorem initoo

Description: An initial object is an object. (Contributed by AV, 14-Apr-2020)

Ref Expression
Assertion initoo ⊢C∈Cat→O∈InitO⁡C→O∈BaseC

Proof

Step Hyp Ref Expression
1 eqid ⊢BaseC=BaseC
2 eqid ⊢Hom⁡C=Hom⁡C
3 id ⊢C∈Cat→C∈Cat
4 1 2 3 isinitoi ⊢C∈Cat∧O∈InitO⁡C→O∈BaseC∧∀b∈BaseC∃!hh∈OHom⁡Cb
5 4 simpld ⊢C∈Cat∧O∈InitO⁡C→O∈BaseC
6 5 ex ⊢C∈Cat→O∈InitO⁡C→O∈BaseC