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	$⊢ φ \to C \in Cat$
		initoeu1.a	$⊢ φ \to A \in InitO (C)$
		initoeu1.b	$⊢ φ \to B \in InitO (C)$
	Assertion	initoeu1w	$⊢ φ \to A ≃_{𝑐} (C) B$

Proof

Step	Hyp	Ref	Expression
1		initoeu1.c	$⊢ φ \to C \in Cat$
2		initoeu1.a	$⊢ φ \to A \in InitO (C)$
3		initoeu1.b	$⊢ φ \to B \in InitO (C)$
4	1 2 3	initoeu1	$⊢ φ \to \exists! f f \in (A Iso (C) B)$
5		euex	$⊢ \exists! f f \in (A Iso (C) B) \to \exists f f \in (A Iso (C) B)$
6	4 5	syl	$⊢ φ \to \exists f f \in (A Iso (C) B)$
7		eqid	$⊢ Iso (C) = Iso (C)$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9		initoo	$⊢ C \in Cat \to (A \in InitO (C) \to A \in {Base}_{C})$
10	1 2 9	sylc	$⊢ φ \to A \in {Base}_{C}$
11		initoo	$⊢ C \in Cat \to (B \in InitO (C) \to B \in {Base}_{C})$
12	1 3 11	sylc	$⊢ φ \to B \in {Base}_{C}$
13	7 8 1 10 12	cic	$⊢ φ \to (A ≃_{𝑐} (C) B \leftrightarrow \exists f f \in (A Iso (C) B))$
14	6 13	mpbird	$⊢ φ \to A ≃_{𝑐} (C) B$