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 = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccic | |- ~=c |
|
| 1 | vc | |- c |
|
| 2 | ccat | |- Cat |
|
| 3 | ciso | |- Iso |
|
| 4 | 1 | cv | |- c |
| 5 | 4 3 | cfv | |- ( Iso ` c ) |
| 6 | csupp | |- supp |
|
| 7 | c0 | |- (/) |
|
| 8 | 5 7 6 | co | |- ( ( Iso ` c ) supp (/) ) |
| 9 | 1 2 8 | cmpt | |- ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) ) |
| 10 | 0 9 | wceq | |- ~=c = ( c e. Cat |-> ( ( Iso ` c ) supp (/) ) ) |