Description: Objects X and Y in a category are isomorphic provided that there is an isomorphism f : X --> Y , see definition 3.15 of Adamek p. 29. (Contributed by AV, 4-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cic.i | |- I = ( Iso ` C ) |
|
cic.b | |- B = ( Base ` C ) |
||
cic.c | |- ( ph -> C e. Cat ) |
||
cic.x | |- ( ph -> X e. B ) |
||
cic.y | |- ( ph -> Y e. B ) |
||
Assertion | cic | |- ( ph -> ( X ( ~=c ` C ) Y <-> E. f f e. ( X I Y ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cic.i | |- I = ( Iso ` C ) |
|
2 | cic.b | |- B = ( Base ` C ) |
|
3 | cic.c | |- ( ph -> C e. Cat ) |
|
4 | cic.x | |- ( ph -> X e. B ) |
|
5 | cic.y | |- ( ph -> Y e. B ) |
|
6 | 1 2 3 4 5 | brcic | |- ( ph -> ( X ( ~=c ` C ) Y <-> ( X I Y ) =/= (/) ) ) |
7 | n0 | |- ( ( X I Y ) =/= (/) <-> E. f f e. ( X I Y ) ) |
|
8 | 6 7 | bitrdi | |- ( ph -> ( X ( ~=c ` C ) Y <-> E. f f e. ( X I Y ) ) ) |