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

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 
|- ( ph -> C e. Cat )
termoeu1.a 
|- ( ph -> A e. ( TermO ` C ) )
termoeu1.b 
|- ( ph -> B e. ( TermO ` C ) )
Assertion termoeu1w 
|- ( ph -> A ( ~=c ` C ) B )

Proof

Step Hyp Ref Expression
1 termoeu1.c 
 |-  ( ph -> C e. Cat )
2 termoeu1.a 
 |-  ( ph -> A e. ( TermO ` C ) )
3 termoeu1.b 
 |-  ( ph -> B e. ( TermO ` C ) )
4 1 2 3 termoeu1 
 |-  ( ph -> E! f f e. ( A ( Iso ` C ) B ) )
5 euex 
 |-  ( E! f f e. ( A ( Iso ` C ) B ) -> E. f f e. ( A ( Iso ` C ) B ) )
6 4 5 syl 
 |-  ( ph -> E. f f e. ( A ( Iso ` C ) B ) )
7 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 termoo 
 |-  ( C e. Cat -> ( A e. ( TermO ` C ) -> A e. ( Base ` C ) ) )
10 1 2 9 sylc 
 |-  ( ph -> A e. ( Base ` C ) )
11 termoo 
 |-  ( C e. Cat -> ( B e. ( TermO ` C ) -> B e. ( Base ` C ) ) )
12 1 3 11 sylc 
 |-  ( ph -> B e. ( Base ` C ) )
13 7 8 1 10 12 cic 
 |-  ( ph -> ( A ( ~=c ` C ) B <-> E. f f e. ( A ( Iso ` C ) B ) ) )
14 6 13 mpbird 
 |-  ( ph -> A ( ~=c ` C ) B )