Description: Prove that two objects are isomorphic by an explicit isomorphism. (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 ) |
||
cic.f | |- ( ph -> F e. ( X I Y ) ) |
||
Assertion | brcici | |- ( ph -> X ( ~=c ` C ) 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 | cic.f | |- ( ph -> F e. ( X I Y ) ) |
|
7 | eleq1 | |- ( f = F -> ( f e. ( X I Y ) <-> F e. ( X I Y ) ) ) |
|
8 | 7 | spcegv | |- ( F e. ( X I Y ) -> ( F e. ( X I Y ) -> E. f f e. ( X I Y ) ) ) |
9 | 6 6 8 | sylc | |- ( ph -> E. f f e. ( X I Y ) ) |
10 | 1 2 3 4 5 | cic | |- ( ph -> ( X ( ~=c ` C ) Y <-> E. f f e. ( X I Y ) ) ) |
11 | 9 10 | mpbird | |- ( ph -> X ( ~=c ` C ) Y ) |