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 )