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 | |- ( 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 ) |
| 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 ) |