Description: Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cic.i | |
|
cic.b | |
||
cic.c | |
||
cic.x | |
||
cic.y | |
||
cic.f | |
||
Assertion | brcici | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cic.i | |
|
2 | cic.b | |
|
3 | cic.c | |
|
4 | cic.x | |
|
5 | cic.y | |
|
6 | cic.f | |
|
7 | eleq1 | |
|
8 | 7 | spcegv | |
9 | 6 6 8 | sylc | |
10 | 1 2 3 4 5 | cic | |
11 | 9 10 | mpbird | |