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	⊢ ≃𝑐 = ( 𝑐 ∈ Cat ↦ ( ( Iso ‘ 𝑐 ) supp ∅ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccic	⊢ ≃𝑐
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		ciso	⊢ Iso
4	1	cv	⊢ 𝑐
5	4 3	cfv	⊢ ( Iso ‘ 𝑐 )
6		csupp	⊢ supp
7		c0	⊢ ∅
8	5 7 6	co	⊢ ( ( Iso ‘ 𝑐 ) supp ∅ )
9	1 2 8	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( ( Iso ‘ 𝑐 ) supp ∅ ) )
10	0 9	wceq	⊢ ≃𝑐 = ( 𝑐 ∈ Cat ↦ ( ( Iso ‘ 𝑐 ) supp ∅ ) )