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

Proof

Step	Hyp	Ref	Expression
1		termoeu1.c	$⊢ φ \to C \in Cat$
2		termoeu1.a	$⊢ φ \to A \in TermO (C)$
3		termoeu1.b	$⊢ φ \to B \in TermO (C)$
4	1 2 3	termoeu1	$⊢ φ \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		termoo	$⊢ C \in Cat \to (A \in TermO (C) \to A \in {Base}_{C})$
10	1 2 9	sylc	$⊢ φ \to A \in {Base}_{C}$
11		termoo	$⊢ C \in Cat \to (B \in TermO (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$