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	$⊢ ≃_{𝑐} = (c \in Cat ⟼ Iso (c) supp \emptyset)$

Detailed syntax breakdown

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