This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐶 ∈ 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 ⊢ ( 𝜑 → 𝐶 ( ≃𝑐 ‘ 𝐸 ) 𝑄 )