Metamath Proof Explorer


Theorem initoo

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

Ref Expression
Assertion initoo ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
2 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
3 id ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
4 1 2 3 isinitoi ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ∈ ( 𝑂 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
5 4 simpld ( ( 𝐶 ∈ Cat ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → 𝑂 ∈ ( Base ‘ 𝐶 ) )
6 5 ex ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )