Metamath Proof Explorer

Theorem cicsym

Description: Isomorphism is symmetric. (Contributed by AV, 5-Apr-2020)

Ref Expression
Assertion cicsym 
|- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S ( ~=c ` C ) R )

Proof

Step Hyp Ref Expression
1 cicrcl 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S e. ( Base ` C ) )
2 ciclcl 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> R e. ( Base ` C ) )
3 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 simpl 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> C e. Cat )
6 simpr 
 |-  ( ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) -> R e. ( Base ` C ) )
7 6 adantl 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> R e. ( Base ` C ) )
8 simpl 
 |-  ( ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) -> S e. ( Base ` C ) )
9 8 adantl 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> S e. ( Base ` C ) )
10 3 4 5 7 9 cic 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( R ( ~=c ` C ) S <-> E. f f e. ( R ( Iso ` C ) S ) ) )
11 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
12 4 11 5 7 9 3 isoval 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( R ( Iso ` C ) S ) = dom ( R ( Inv ` C ) S ) )
13 4 11 5 9 7 invsym2 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> `' ( S ( Inv ` C ) R ) = ( R ( Inv ` C ) S ) )
14 13 eqcomd 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( R ( Inv ` C ) S ) = `' ( S ( Inv ` C ) R ) )
15 14 dmeqd 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> dom ( R ( Inv ` C ) S ) = dom `' ( S ( Inv ` C ) R ) )
16 df-rn 
 |-  ran ( S ( Inv ` C ) R ) = dom `' ( S ( Inv ` C ) R )
17 15 16 eqtr4di 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> dom ( R ( Inv ` C ) S ) = ran ( S ( Inv ` C ) R ) )
18 12 17 eqtrd 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( R ( Iso ` C ) S ) = ran ( S ( Inv ` C ) R ) )
19 18 eleq2d 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( f e. ( R ( Iso ` C ) S ) <-> f e. ran ( S ( Inv ` C ) R ) ) )
20 vex 
 |-  f e. _V
21 elrng 
 |-  ( f e. _V -> ( f e. ran ( S ( Inv ` C ) R ) <-> E. g g ( S ( Inv ` C ) R ) f ) )
22 20 21 mp1i 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( f e. ran ( S ( Inv ` C ) R ) <-> E. g g ( S ( Inv ` C ) R ) f ) )
23 19 22 bitrd 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( f e. ( R ( Iso ` C ) S ) <-> E. g g ( S ( Inv ` C ) R ) f ) )
24 df-br 
 |-  ( g ( S ( Inv ` C ) R ) f <-> <. g , f >. e. ( S ( Inv ` C ) R ) )
25 24 exbii 
 |-  ( E. g g ( S ( Inv ` C ) R ) f <-> E. g <. g , f >. e. ( S ( Inv ` C ) R ) )
26 vex 
 |-  g e. _V
27 26 20 opeldm 
 |-  ( <. g , f >. e. ( S ( Inv ` C ) R ) -> g e. dom ( S ( Inv ` C ) R ) )
28 4 11 5 9 7 3 isoval 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( S ( Iso ` C ) R ) = dom ( S ( Inv ` C ) R ) )
29 28 eqcomd 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> dom ( S ( Inv ` C ) R ) = ( S ( Iso ` C ) R ) )
30 29 eleq2d 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( g e. dom ( S ( Inv ` C ) R ) <-> g e. ( S ( Iso ` C ) R ) ) )
31 5 adantr 
 |-  ( ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) /\ g e. ( S ( Iso ` C ) R ) ) -> C e. Cat )
32 9 adantr 
 |-  ( ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) /\ g e. ( S ( Iso ` C ) R ) ) -> S e. ( Base ` C ) )
33 7 adantr 
 |-  ( ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) /\ g e. ( S ( Iso ` C ) R ) ) -> R e. ( Base ` C ) )
34 simpr 
 |-  ( ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) /\ g e. ( S ( Iso ` C ) R ) ) -> g e. ( S ( Iso ` C ) R ) )
35 3 4 31 32 33 34 brcici 
 |-  ( ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) /\ g e. ( S ( Iso ` C ) R ) ) -> S ( ~=c ` C ) R )
36 35 ex 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( g e. ( S ( Iso ` C ) R ) -> S ( ~=c ` C ) R ) )
37 30 36 sylbid 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( g e. dom ( S ( Inv ` C ) R ) -> S ( ~=c ` C ) R ) )
38 27 37 syl5com 
 |-  ( <. g , f >. e. ( S ( Inv ` C ) R ) -> ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> S ( ~=c ` C ) R ) )
39 38 exlimiv 
 |-  ( E. g <. g , f >. e. ( S ( Inv ` C ) R ) -> ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> S ( ~=c ` C ) R ) )
40 39 com12 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( E. g <. g , f >. e. ( S ( Inv ` C ) R ) -> S ( ~=c ` C ) R ) )
41 25 40 syl5bi 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( E. g g ( S ( Inv ` C ) R ) f -> S ( ~=c ` C ) R ) )
42 23 41 sylbid 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( f e. ( R ( Iso ` C ) S ) -> S ( ~=c ` C ) R ) )
43 42 exlimdv 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( E. f f e. ( R ( Iso ` C ) S ) -> S ( ~=c ` C ) R ) )
44 10 43 sylbid 
 |-  ( ( C e. Cat /\ ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) ) -> ( R ( ~=c ` C ) S -> S ( ~=c ` C ) R ) )
45 44 impancom 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> ( ( S e. ( Base ` C ) /\ R e. ( Base ` C ) ) -> S ( ~=c ` C ) R ) )
46 1 2 45 mp2and 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S ( ~=c ` C ) R )