Theorem termoo2

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

	Ref	Expression
Hypothesis	initoo2.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	termoo2	⊢ ( 𝑂 ∈ ( TermO ‘ 𝐶 ) → 𝑂 ∈ 𝐵 )

Proof

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