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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diagffth.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	diagffth.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
	diagciso.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
	diagciso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	diagciso.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	diagciso.1	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
Assertion	diagcic	⊢ ( 𝜑 → 𝐶 ( ≃𝑐 ‘ 𝐸 ) 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		diagffth.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3		diagffth.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
4		diagciso.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
5		diagciso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6		diagciso.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
7		diagciso.1	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
8		eqid	⊢ ( Iso ‘ 𝐸 ) = ( Iso ‘ 𝐸 )
9		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
10	4	catccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐸 ∈ Cat )
11	5 10	syl	⊢ ( 𝜑 → 𝐸 ∈ Cat )
12	6 1	elind	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∩ Cat ) )
13	4 9 5	catcbas	⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
14	12 13	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐸 ) )
15	2	termccd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	3 15 1	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
17	7 16	elind	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑈 ∩ Cat ) )
18	17 13	eleqtrrd	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐸 ) )
19		eqid	⊢ ( 𝐶 Δfunc 𝐷 ) = ( 𝐶 Δfunc 𝐷 )
20	1 2 3 4 5 6 7 8 19	diagciso	⊢ ( 𝜑 → ( 𝐶 Δfunc 𝐷 ) ∈ ( 𝐶 ( Iso ‘ 𝐸 ) 𝑄 ) )
21	8 9 11 14 18 20	brcici	⊢ ( 𝜑 → 𝐶 ( ≃𝑐 ‘ 𝐸 ) 𝑄 )