This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
initoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
Assertion initoeu1w ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 initoeu1.a ⊢ ( 𝜑 → 𝐴 ∈ ( InitO ‘ 𝐶 ) )
3 initoeu1.b ⊢ ( 𝜑 → 𝐵 ∈ ( InitO ‘ 𝐶 ) )
4 1 2 3 initoeu1 ⊢ ( 𝜑 → ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
5 euex ⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
6 4 5 syl ⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) )
7 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 initoo ⊢ ( 𝐶 ∈ Cat → ( 𝐴 ∈ ( InitO ‘ 𝐶 ) → 𝐴 ∈ ( Base ‘ 𝐶 ) ) )
10 1 2 9 sylc ⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐶 ) )
11 initoo ⊢ ( 𝐶 ∈ Cat → ( 𝐵 ∈ ( InitO ‘ 𝐶 ) → 𝐵 ∈ ( Base ‘ 𝐶 ) ) )
12 1 3 11 sylc ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ 𝐶 ) )
13 7 8 1 10 12 cic ⊢ ( 𝜑 → ( 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 ( Iso ‘ 𝐶 ) 𝐵 ) ) )
14 6 13 mpbird ⊢ ( 𝜑 → 𝐴 ( ≃𝑐 ‘ 𝐶 ) 𝐵 )