Definition df-cic 17964

Description: Function returning the set of isomorphic objects for each category 𝑐. Definition 3.15 of [Adamek] p. 29. Analogous to the definition of the group isomorphism relation ≃_𝑔, see df-gic 19467. (Contributed by AV, 4-Apr-2020.)

Assertion

Ref	Expression
df-cic	⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅))

Detailed syntax breakdown of Definition df-cic

Step	Hyp	Ref	Expression
1		ccic 17963	. 2 class ≃𝑐
2		vc	. . 3 setvar 𝑐
3		ccat 17831	. . 3 class Cat
4	2	cv 1569	. . . . 5 class 𝑐
5		ciso 17914	. . . . 5 class Iso
6	4, 5	cfv 6537	. . . 4 class (Iso‘𝑐)
7		c0 4279	. . . 4 class ∅
8		csupp 8170	. . . 4 class supp
9	6, 7, 8	co 7418	. . 3 class ((Iso‘𝑐) supp ∅)
10	2, 3, 9	cmpt 5186	. 2 class (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅))
11	1, 10	wceq 1570	1 wff ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅))

This definition is used by:  cicfval  17965  cicfn  50119