This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ≃𝑐 = ( 𝑐 ∈ 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 ∅ ) )