Metamath Proof Explorer


Theorem cic

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 ) ) )

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 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 ) ) )