Metamath Proof Explorer

Theorem initoeu1w

Description: Initial objects are essentially unique (weak form), i.e. if A and B are initial objects, then A and B are isomorphic. Proposition 7.3 (1) of Adamek p. 102. (Contributed by AV, 6-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ φ → C ∈ Cat
initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
initoeu1.b ⊢ φ → B ∈ InitO ⁡ C
Assertion initoeu1w ⊢ φ → A ≃ 𝑐 ⁡ C B

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ φ → C ∈ Cat
2 initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
3 initoeu1.b ⊢ φ → B ∈ InitO ⁡ C
4 1 2 3 initoeu1 ⊢ φ → ∃! 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 initoo ⊢ C ∈ Cat → A ∈ InitO ⁡ C → A ∈ Base C
10 1 2 9 sylc ⊢ φ → A ∈ Base C
11 initoo ⊢ C ∈ Cat → B ∈ InitO ⁡ 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