termcid

Description: The morphism of a terminal category is an identity morphism. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	termcbas.c	No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
	termcbas.b	$⊢ B = {Base}_{C}$
	termcbasmo.x	$⊢ φ \to X \in B$
	termcbasmo.y	$⊢ φ \to Y \in B$
	termcid.h	$⊢ H = Hom (C)$
	termcid.f	$⊢ φ \to F \in (X H Y)$
	termcid.i	$⊢ \underset{˙}{1} = Id (C)$
Assertion	termcid	$⊢ φ \to F = \underset{˙}{1} (X)$

Step	Hyp	Ref	Expression
1		termcbas.c	Could not format ( ph -> C e. TermCat ) : No typesetting found for \|- ( ph -> C e. TermCat ) with typecode \|-
2		termcbas.b	$⊢ B = {Base}_{C}$
3		termcbasmo.x	$⊢ φ \to X \in B$
4		termcbasmo.y	$⊢ φ \to Y \in B$
5		termcid.h	$⊢ H = Hom (C)$
6		termcid.f	$⊢ φ \to F \in (X H Y)$
7		termcid.i	$⊢ \underset{˙}{1} = Id (C)$
8	1	termcthind	$⊢ φ \to C \in ThinCat$
9	1 2 3 4	termcbasmo	$⊢ φ \to X = Y$
10	9	oveq2d	$⊢ φ \to X H X = X H Y$
11	6 10	eleqtrrd	$⊢ φ \to F \in (X H X)$
12	8 2 5 3 7 11	thincid	$⊢ φ \to F = \underset{˙}{1} (X)$

Metamath Proof Explorer