Metamath Proof Explorer

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 ⊢ B = Base C
Assertion termoo2 ⊢ O ∈ TermO ⁡ C → O ∈ B

Proof

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