Theorem thincid

Description: In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	thincid.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
	thincid.b	$$⊢B={\mathrm{Base}}_C$$
	thincid.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	thincid.x	$$⊢\phi \to X\in B$$
	thincid.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	thincid.f	$$⊢\phi \to F\in \left(XHX\right)$$
Assertion	thincid	$$⊢\phi \to F=\underset{\dot{}}{1}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		thincid.c	$$⊢\phi \to C\in \mathrm{ThinCat}$$
2		thincid.b	$$⊢B={\mathrm{Base}}_C$$
3		thincid.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		thincid.x	$$⊢\phi \to X\in B$$
5		thincid.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
6		thincid.f	$$⊢\phi \to F\in \left(XHX\right)$$
7	1	thinccatd	$$⊢\phi \to C\in \mathrm{Cat}$$
8	2 3 5 7 4	catidcl	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \left(XHX\right)$$
9	4 4 6 8 2 3 1	thincmo2	$$⊢\phi \to F=\underset{\dot{}}{1}\left(X\right)$$