Definition df-cic 16456

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 17702. (Contributed by AV, 4-Apr-2020.)

Assertion

Ref	Expression
df-cic	|- ~=c𝑐 = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) )

Detailed syntax breakdown of Definition df-cic

Step	Hyp	Ref	Expression
1		ccic 16455	. 2 class ~=c𝑐
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4	2	cv 1482	. . . . 5 class c
5		ciso 16406	. . . . 5 class Iso
6	4, 5	cfv 5888	. . . 4 class ( Iso ` c )
7		c0 3915	. . . 4 class (/)
8		csupp 7295	. . . 4 class supp
9	6, 7, 8	co 6650	. . 3 class ( ( Iso ` c ) supp (/) )
10	2, 3, 9	cmpt 4729	. 2 class ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) )
11	1, 10	wceq 1483	1 wff ~=c𝑐 = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) )

This definition is referenced by:  cicfval  16457