termccisoeu

Description: The isomorphism between terminal categories is unique. (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	termcciso.c	$⊢ C = CatCat (U)$
	termcciso.b	$⊢ B = {Base}_{C}$
	termcciso.x	$⊢ φ \to X \in B$
	termcciso.y	$⊢ φ \to Y \in B$
	termcciso.t	No typesetting found for \|- ( ph -> X e. TermCat ) with typecode \|-
	termccisoeu.y	No typesetting found for \|- ( ph -> Y e. TermCat ) with typecode \|-
Assertion	termccisoeu	$⊢ φ \to \exists! f f \in (X Iso (C) Y)$

Step	Hyp	Ref	Expression
1		termcciso.c	$⊢ C = CatCat (U)$
2		termcciso.b	$⊢ B = {Base}_{C}$
3		termcciso.x	$⊢ φ \to X \in B$
4		termcciso.y	$⊢ φ \to Y \in B$
5		termcciso.t	Could not format ( ph -> X e. TermCat ) : No typesetting found for \|- ( ph -> X e. TermCat ) with typecode \|-
6		termccisoeu.y	Could not format ( ph -> Y e. TermCat ) : No typesetting found for \|- ( ph -> Y e. TermCat ) with typecode \|-
7	1 2	elbasfv	$⊢ X \in B \to U \in V$
8	3 7	syl	$⊢ φ \to U \in V$
9	1	catccat	$⊢ U \in V \to C \in Cat$
10	8 9	syl	$⊢ φ \to C \in Cat$
11	1 2 8	catcbas	$⊢ φ \to B = U \cap Cat$
12	3 11	eleqtrd	$⊢ φ \to X \in (U \cap Cat)$
13	12	elin1d	$⊢ φ \to X \in U$
14	1 8 13 5	termcterm	$⊢ φ \to X \in TermO (C)$
15	4 11	eleqtrd	$⊢ φ \to Y \in (U \cap Cat)$
16	15	elin1d	$⊢ φ \to Y \in U$
17	1 8 16 6	termcterm	$⊢ φ \to Y \in TermO (C)$
18	10 14 17	termoeu1	$⊢ φ \to \exists! f f \in (X Iso (C) Y)$

Metamath Proof Explorer