Metamath Proof Explorer


Theorem brcic

Description: The relation "is isomorphic to" for categories. (Contributed by AV, 5-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 brcic
|- ( ph -> ( X ( ~=c ` C ) Y <-> ( 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 cicfval
 |-  ( C e. Cat -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) )
7 3 6 syl
 |-  ( ph -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) )
8 7 breqd
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> X ( ( Iso ` C ) supp (/) ) Y ) )
9 df-br
 |-  ( X ( ( Iso ` C ) supp (/) ) Y <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) )
10 9 a1i
 |-  ( ph -> ( X ( ( Iso ` C ) supp (/) ) Y <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) )
11 1 a1i
 |-  ( ph -> I = ( Iso ` C ) )
12 11 fveq1d
 |-  ( ph -> ( I ` <. X , Y >. ) = ( ( Iso ` C ) ` <. X , Y >. ) )
13 12 neeq1d
 |-  ( ph -> ( ( I ` <. X , Y >. ) =/= (/) <-> ( ( Iso ` C ) ` <. X , Y >. ) =/= (/) ) )
14 df-ov
 |-  ( X I Y ) = ( I ` <. X , Y >. )
15 14 eqcomi
 |-  ( I ` <. X , Y >. ) = ( X I Y )
16 15 a1i
 |-  ( ph -> ( I ` <. X , Y >. ) = ( X I Y ) )
17 16 neeq1d
 |-  ( ph -> ( ( I ` <. X , Y >. ) =/= (/) <-> ( X I Y ) =/= (/) ) )
18 fvexd
 |-  ( ph -> ( Base ` C ) e. _V )
19 18 18 xpexd
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) e. _V )
20 4 2 eleqtrdi
 |-  ( ph -> X e. ( Base ` C ) )
21 5 2 eleqtrdi
 |-  ( ph -> Y e. ( Base ` C ) )
22 20 21 opelxpd
 |-  ( ph -> <. X , Y >. e. ( ( Base ` C ) X. ( Base ` C ) ) )
23 isofn
 |-  ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
24 3 23 syl
 |-  ( ph -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
25 fvn0elsuppb
 |-  ( ( ( ( Base ` C ) X. ( Base ` C ) ) e. _V /\ <. X , Y >. e. ( ( Base ` C ) X. ( Base ` C ) ) /\ ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) -> ( ( ( Iso ` C ) ` <. X , Y >. ) =/= (/) <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) )
26 19 22 24 25 syl3anc
 |-  ( ph -> ( ( ( Iso ` C ) ` <. X , Y >. ) =/= (/) <-> <. X , Y >. e. ( ( Iso ` C ) supp (/) ) ) )
27 13 17 26 3bitr3rd
 |-  ( ph -> ( <. X , Y >. e. ( ( Iso ` C ) supp (/) ) <-> ( X I Y ) =/= (/) ) )
28 8 10 27 3bitrd
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> ( X I Y ) =/= (/) ) )