Metamath Proof Explorer

Theorem termoeu1w

Description: Terminal objects are essentially unique (weak form), i.e. if A and B are terminal objects, then A and B are isomorphic. Proposition 7.6 of Adamek p. 103. (Contributed by AV, 18-Apr-2020)

Ref Expression
Hypotheses termoeu1.c ⊢ φ → C ∈ Cat
termoeu1.a ⊢ φ → A ∈ TermO ⁡ C
termoeu1.b ⊢ φ → B ∈ TermO ⁡ C
Assertion termoeu1w ⊢ φ → A ≃ 𝑐 ⁡ C B

Proof

Step Hyp Ref Expression
1 termoeu1.c ⊢ φ → C ∈ Cat
2 termoeu1.a ⊢ φ → A ∈ TermO ⁡ C
3 termoeu1.b ⊢ φ → B ∈ TermO ⁡ C
4 1 2 3 termoeu1 ⊢ φ → ∃! f f ∈ A Iso ⁡ C B
5 euex ⊢ ∃! f f ∈ A Iso ⁡ C B → ∃ f f ∈ A Iso ⁡ C B
6 4 5 syl ⊢ φ → ∃ f f ∈ A Iso ⁡ C B
7 eqid ⊢ Iso ⁡ C = Iso ⁡ C
8 eqid ⊢ Base C = Base C
9 termoo ⊢ C ∈ Cat → A ∈ TermO ⁡ C → A ∈ Base C
10 1 2 9 sylc ⊢ φ → A ∈ Base C
11 termoo ⊢ C ∈ Cat → B ∈ TermO ⁡ C → B ∈ Base C
12 1 3 11 sylc ⊢ φ → B ∈ Base C
13 7 8 1 10 12 cic ⊢ φ → A ≃ 𝑐 ⁡ C B ↔ ∃ f f ∈ A Iso ⁡ C B
14 6 13 mpbird ⊢ φ → A ≃ 𝑐 ⁡ C B