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	|- ( ph -> C e. Cat )
	diagffth.d	|- ( ph -> D e. TermCat )
	diagffth.q	|- Q = ( D FuncCat C )
	diagciso.e	|- E = ( CatCat ` U )
	diagciso.u	|- ( ph -> U e. V )
	diagciso.c	|- ( ph -> C e. U )
	diagciso.1	|- ( ph -> Q e. U )
Assertion	diagcic	|- ( ph -> C ( ~=c ` E ) Q )

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	|- ( ph -> C e. Cat )
2		diagffth.d	|- ( ph -> D e. TermCat )
3		diagffth.q	|- Q = ( D FuncCat C )
4		diagciso.e	|- E = ( CatCat ` U )
5		diagciso.u	|- ( ph -> U e. V )
6		diagciso.c	|- ( ph -> C e. U )
7		diagciso.1	|- ( ph -> Q e. U )
8		eqid	|- ( Iso ` E ) = ( Iso ` E )
9		eqid	|- ( Base ` E ) = ( Base ` E )
10	4	catccat	|- ( U e. V -> E e. Cat )
11	5 10	syl	|- ( ph -> E e. Cat )
12	6 1	elind	|- ( ph -> C e. ( U i^i Cat ) )
13	4 9 5	catcbas	|- ( ph -> ( Base ` E ) = ( U i^i Cat ) )
14	12 13	eleqtrrd	|- ( ph -> C e. ( Base ` E ) )
15	2	termccd	|- ( ph -> D e. Cat )
16	3 15 1	fuccat	|- ( ph -> Q e. Cat )
17	7 16	elind	|- ( ph -> Q e. ( U i^i Cat ) )
18	17 13	eleqtrrd	|- ( ph -> Q e. ( Base ` E ) )
19		eqid	|- ( C DiagFunc D ) = ( C DiagFunc D )
20	1 2 3 4 5 6 7 8 19	diagciso	|- ( ph -> ( C DiagFunc D ) e. ( C ( Iso ` E ) Q ) )
21	8 9 11 14 18 20	brcici	|- ( ph -> C ( ~=c ` E ) Q )