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 ( 𝜑𝐶 ∈ Cat )
termoeu1.a ( 𝜑𝐴 ∈ ( TermO ‘ 𝐶 ) )
termoeu1.b ( 𝜑𝐵 ∈ ( TermO ‘ 𝐶 ) )
Assertion termoeu1w ( 𝜑𝐴 ( ≃𝑐𝐶 ) 𝐵 )

Proof

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