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

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 ) =/= (/) ) )