Metamath Proof Explorer

Theorem termoo

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

Ref Expression
Assertion termoo ⊢ C ∈ Cat → O ∈ TermO ⁡ C → O ∈ Base C

Proof

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