Metamath Proof Explorer

Theorem termoeu2

Description: Terminal objects are essentially unique; if A is a terminal object, then so is every object that is isomorphic to A . (Contributed by Zhi Wang, 26-Oct-2025)

Ref Expression
Hypotheses termoeu2.c ⊢ φ → C ∈ Cat
termoeu2.a ⊢ φ → A ∈ TermO ⁡ C
termoeu2.i ⊢ φ → A ≃ 𝑐 ⁡ C B
Assertion termoeu2 ⊢ φ → B ∈ TermO ⁡ C

Proof

Step Hyp Ref Expression
1 termoeu2.c ⊢ φ → C ∈ Cat
2 termoeu2.a ⊢ φ → A ∈ TermO ⁡ C
3 termoeu2.i ⊢ φ → A ≃ 𝑐 ⁡ C B
4 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
5 4 oppccat ⊢ C ∈ Cat → oppCat ⁡ C ∈ Cat
6 1 5 syl ⊢ φ → oppCat ⁡ C ∈ Cat
7 oppctermo ⊢ A ∈ TermO ⁡ C ↔ A ∈ InitO ⁡ oppCat ⁡ C
8 2 7 sylib ⊢ φ → A ∈ InitO ⁡ oppCat ⁡ C
9 4 3 oppccic ⊢ φ → A ≃ 𝑐 ⁡ oppCat ⁡ C B
10 6 8 9 initoeu2 ⊢ φ → B ∈ InitO ⁡ oppCat ⁡ C
11 oppctermo ⊢ B ∈ TermO ⁡ C ↔ B ∈ InitO ⁡ oppCat ⁡ C
12 10 11 sylibr ⊢ φ → B ∈ TermO ⁡ C