Theorem termoo

Description: A terminal object is an object. (Contributed by AV, 18-Apr-2020)

	Ref	Expression
Assertion	termoo	⊢ ( 𝐶 ∈ Cat → ( 𝑂 ∈ ( TermO ‘ 𝐶 ) → 𝑂 ∈ ( Base ‘ 𝐶 ) ) )

Proof

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