Theorem idfudiag1bas

Description: If the identity functor of a category is the same as a constant functor to the category, then the base is a singleton. (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	idfudiag1.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	idfudiag1.l	$$⊢L=C{\Delta }_{\mathrm{func}}C$$
	idfudiag1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	idfudiag1.b	$$⊢B={\mathrm{Base}}_C$$
	idfudiag1.x	$$⊢\phi \to X\in B$$
	idfudiag1.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
	idfudiag1.e	$$⊢\phi \to I=K$$
Assertion	idfudiag1bas	$$⊢\phi \to B=\left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		idfudiag1.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idfudiag1.l	$$⊢L=C{\Delta }_{\mathrm{func}}C$$
3		idfudiag1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		idfudiag1.b	$$⊢B={\mathrm{Base}}_C$$
5		idfudiag1.x	$$⊢\phi \to X\in B$$
6		idfudiag1.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
7		idfudiag1.e	$$⊢\phi \to I=K$$
8		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
9	1 4 3 8	idfuval	$$⊢\phi \to I=⟨{\mathrm{I}\upharpoonright }_B,\left(p\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(p\right)}\right)⟩$$
10		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
11	2 3 3 4 5 6 4 8 10	diag1a	$$⊢\phi \to K=⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(C\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩$$
12	7 9 11	3eqtr3d	$$⊢\phi \to ⟨{\mathrm{I}\upharpoonright }_B,\left(p\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(p\right)}\right)⟩=⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(C\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩$$
13	4	fvexi	$$⊢B\in \mathrm{V}$$
14		resiexg	$$⊢B\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
15	13 14	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
16	13 13	xpex	$$⊢B\times B\in \mathrm{V}$$
17	16	mptex	$$⊢\left(p\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(p\right)}\right)\in \mathrm{V}$$
18	15 17	opth1	$$⊢⟨{\mathrm{I}\upharpoonright }_B,\left(p\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(p\right)}\right)⟩=⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(y\mathrm{Hom}\left(C\right)z\right)\times \left\{\mathrm{Id}\left(C\right)\left(X\right)\right\}\right)⟩\to {\mathrm{I}\upharpoonright }_B=B\times \left\{X\right\}$$
19	12 18	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_B=B\times \left\{X\right\}$$
20	5	ne0d	$$⊢\phi \to B\ne \varnothing$$
21	19 20	idfudiag1lem	$$⊢\phi \to B=\left\{X\right\}$$