This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brcici

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 )

Proof

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 )