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	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		ciso	$$class\mathrm{Iso}$$
4	1	cv	$$setvarc$$
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)$$