Metamath Proof Explorer

Definition df-cic

Description: Function returning the set of isomorphic objects for each category c . Definition 3.15 of Adamek p. 29. Analogous to the definition of the group isomorphism relation ~=g , see df-gic . (Contributed by AV, 4-Apr-2020)

Ref Expression
Assertion df-cic ${⊢}{\simeq }_{𝑐}=\left({c}\in \mathrm{Cat}⟼\mathrm{Iso}\left({c}\right)\mathrm{supp}\varnothing \right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccic ${class}{\simeq }_{𝑐}$
1 vc ${setvar}{c}$
2 ccat ${class}\mathrm{Cat}$
3 ciso ${class}\mathrm{Iso}$
4 1 cv ${setvar}{c}$
5 4 3 cfv ${class}\mathrm{Iso}\left({c}\right)$
6 csupp ${class}\mathrm{supp}$
7 c0 ${class}\varnothing$
8 5 7 6 co ${class}{supp}_{\varnothing }\left(\mathrm{Iso}\left({c}\right)\right)$
9 1 2 8 cmpt ${class}\left({c}\in \mathrm{Cat}⟼\mathrm{Iso}\left({c}\right)\mathrm{supp}\varnothing \right)$
10 0 9 wceq ${wff}{\simeq }_{𝑐}=\left({c}\in \mathrm{Cat}⟼\mathrm{Iso}\left({c}\right)\mathrm{supp}\varnothing \right)$