Theorem diagcic

Description: Any category C is isomorphic to the category of functors from a terminal category to C . Therefore the number of categories isomorphic to a non-empty category is at least the number of singletons, so large ( snnex ) that these isomorphic categories form a proper class. (Contributed by Zhi Wang, 21-Oct-2025)

	Ref	Expression
Hypotheses	diagffth.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diagffth.d	No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
	diagffth.q	$$⊢Q=D\mathrm{FuncCat}C$$
	diagciso.e	$$⊢E=\mathrm{CatCat}\left(U\right)$$
	diagciso.u	$$⊢\phi \to U\in V$$
	diagciso.c	$$⊢\phi \to C\in U$$
	diagciso.1	$$⊢\phi \to Q\in U$$
Assertion	diagcic	$$⊢\phi \to C{\simeq }_{𝑐}\left(E\right)Q$$

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		diagffth.d	Could not format ( ph -> D e. TermCat ) : No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
3		diagffth.q	$$⊢Q=D\mathrm{FuncCat}C$$
4		diagciso.e	$$⊢E=\mathrm{CatCat}\left(U\right)$$
5		diagciso.u	$$⊢\phi \to U\in V$$
6		diagciso.c	$$⊢\phi \to C\in U$$
7		diagciso.1	$$⊢\phi \to Q\in U$$
8		eqid	$$⊢\mathrm{Iso}\left(E\right)=\mathrm{Iso}\left(E\right)$$
9		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
10	4	catccat	$$⊢U\in V\to E\in \mathrm{Cat}$$
11	5 10	syl	$$⊢\phi \to E\in \mathrm{Cat}$$
12	6 1	elind	$$⊢\phi \to C\in \left(U\cap \mathrm{Cat}\right)$$
13	4 9 5	catcbas	$$⊢\phi \to {\mathrm{Base}}_E=U\cap \mathrm{Cat}$$
14	12 13	eleqtrrd	$$⊢\phi \to C\in {\mathrm{Base}}_E$$
15	2	termccd	$$⊢\phi \to D\in \mathrm{Cat}$$
16	3 15 1	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
17	7 16	elind	$$⊢\phi \to Q\in \left(U\cap \mathrm{Cat}\right)$$
18	17 13	eleqtrrd	$$⊢\phi \to Q\in {\mathrm{Base}}_E$$
19		eqid	$$⊢C{\Delta }_{\mathrm{func}}D=C{\Delta }_{\mathrm{func}}D$$
20	1 2 3 4 5 6 7 8 19	diagciso	$$⊢\phi \to C{\Delta }_{\mathrm{func}}D\in \left(C\mathrm{Iso}\left(E\right)Q\right)$$
21	8 9 11 14 18 20	brcici	$$⊢\phi \to C{\simeq }_{𝑐}\left(E\right)Q$$