Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-cic | Structured version Visualization version GIF version |
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 18865. (Contributed by AV, 4-Apr-2020.) |
Ref | Expression |
---|---|
df-cic | ⊢ ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccic 17496 | . 2 class ≃𝑐 | |
2 | vc | . . 3 setvar 𝑐 | |
3 | ccat 17362 | . . 3 class Cat | |
4 | 2 | cv 1538 | . . . . 5 class 𝑐 |
5 | ciso 17447 | . . . . 5 class Iso | |
6 | 4, 5 | cfv 6428 | . . . 4 class (Iso‘𝑐) |
7 | c0 4258 | . . . 4 class ∅ | |
8 | csupp 7966 | . . . 4 class supp | |
9 | 6, 7, 8 | co 7269 | . . 3 class ((Iso‘𝑐) supp ∅) |
10 | 2, 3, 9 | cmpt 5158 | . 2 class (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) |
11 | 1, 10 | wceq 1539 | 1 wff ≃𝑐 = (𝑐 ∈ Cat ↦ ((Iso‘𝑐) supp ∅)) |
Colors of variables: wff setvar class |
This definition is referenced by: cicfval 17498 |
Copyright terms: Public domain | W3C validator |