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	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	initoo2	⊢ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		initoo2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
3		initorcl	⊢ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )
4	1 2 3	isinitoi	⊢ ( ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 ∈ 𝐵 ∧ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
5	4	anidms	⊢ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → ( 𝑂 ∈ 𝐵 ∧ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 ( Hom ‘ 𝐶 ) 𝑏 ) ) )
6	5	simpld	⊢ ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ 𝐵 )