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 ∈ Base C

Proof

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