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

Proof

Step	Hyp	Ref	Expression
1		initoeu1.c	|- ( ph -> C e. Cat )
2		initoeu1.a	|- ( ph -> A e. ( InitO ` C ) )
3		initoeu1.b	|- ( ph -> B e. ( InitO ` C ) )
4	1 2 3	initoeu1	|- ( 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		initoo	|- ( C e. Cat -> ( A e. ( InitO ` C ) -> A e. ( Base ` C ) ) )
10	1 2 9	sylc	|- ( ph -> A e. ( Base ` C ) )
11		initoo	|- ( C e. Cat -> ( B e. ( InitO ` 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 )