Metamath Proof Explorer

Theorem initoo2

Description: An initial object is an object in the base set. (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Hypothesis initoo2.b ⊢ B = Base C
Assertion initoo2 ⊢ O ∈ InitO ⁡ C → O ∈ B

Proof

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