Metamath Proof Explorer

Theorem diagcic

Description: Any category C is isomorphic to the category of functors from a terminal category to C . See also the "Properties" section of https://ncatlab.org/nlab/show/terminal+category . 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 ⊢ φ → C ∈ Cat
diagffth.d No typesetting found for |- ( ph -> D e. TermCat ) with typecode |-
diagffth.q ⊢ Q = D FuncCat C
diagciso.e ⊢ E = CatCat ⁡ U
diagciso.u ⊢ φ → U ∈ V
diagciso.c ⊢ φ → C ∈ U
diagciso.1 ⊢ φ → Q ∈ U
Assertion diagcic ⊢ φ → C ≃ 𝑐 ⁡ E Q

Proof

Step Hyp Ref Expression
1 diagffth.c ⊢ φ → C ∈ 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 FuncCat C
4 diagciso.e ⊢ E = CatCat ⁡ U
5 diagciso.u ⊢ φ → U ∈ V
6 diagciso.c ⊢ φ → C ∈ U
7 diagciso.1 ⊢ φ → Q ∈ U
8 eqid ⊢ Iso ⁡ E = Iso ⁡ E
9 eqid ⊢ Base E = Base E
10 4 catccat ⊢ U ∈ V → E ∈ Cat
11 5 10 syl ⊢ φ → E ∈ Cat
12 6 1 elind ⊢ φ → C ∈ U ∩ Cat
13 4 9 5 catcbas ⊢ φ → Base E = U ∩ Cat
14 12 13 eleqtrrd ⊢ φ → C ∈ Base E
15 2 termccatd ⊢ φ → D ∈ Cat
16 3 15 1 fuccat ⊢ φ → Q ∈ Cat
17 7 16 elind ⊢ φ → Q ∈ U ∩ Cat
18 17 13 eleqtrrd ⊢ φ → Q ∈ Base E
19 eqid ⊢ C Δ func D = C Δ func D
20 1 2 3 4 5 6 7 8 19 diagciso ⊢ φ → C Δ func D ∈ C Iso ⁡ E Q
21 8 9 11 14 18 20 brcici ⊢ φ → C ≃ 𝑐 ⁡ E Q