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

Metamath Proof Explorer

Theorem invsym2

Description: The inverse relation is symmetric. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b 
|- B = ( Base ` C )
invfval.n 
|- N = ( Inv ` C )
invfval.c 
|- ( ph -> C e. Cat )
invss.x 
|- ( ph -> X e. B )
invss.y 
|- ( ph -> Y e. B )
Assertion invsym2 
|- ( ph -> `' ( X N Y ) = ( Y N X ) )

Proof

Step Hyp Ref Expression
1 invfval.b 
 |-  B = ( Base ` C )
2 invfval.n 
 |-  N = ( Inv ` C )
3 invfval.c 
 |-  ( ph -> C e. Cat )
4 invss.x 
 |-  ( ph -> X e. B )
5 invss.y 
 |-  ( ph -> Y e. B )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 1 2 3 5 4 6 invss 
 |-  ( ph -> ( Y N X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) )
8 relxp 
 |-  Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) )
9 relss 
 |-  ( ( Y N X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> ( Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> Rel ( Y N X ) ) )
10 7 8 9 mpisyl 
 |-  ( ph -> Rel ( Y N X ) )
11 relcnv 
 |-  Rel `' ( X N Y )
12 10 11 jctil 
 |-  ( ph -> ( Rel `' ( X N Y ) /\ Rel ( Y N X ) ) )
13 1 2 3 4 5 invsym 
 |-  ( ph -> ( f ( X N Y ) g <-> g ( Y N X ) f ) )
14 vex 
 |-  g e. _V
15 vex 
 |-  f e. _V
16 14 15 brcnv 
 |-  ( g `' ( X N Y ) f <-> f ( X N Y ) g )
17 df-br 
 |-  ( g `' ( X N Y ) f <-> <. g , f >. e. `' ( X N Y ) )
18 16 17 bitr3i 
 |-  ( f ( X N Y ) g <-> <. g , f >. e. `' ( X N Y ) )
19 df-br 
 |-  ( g ( Y N X ) f <-> <. g , f >. e. ( Y N X ) )
20 13 18 19 3bitr3g 
 |-  ( ph -> ( <. g , f >. e. `' ( X N Y ) <-> <. g , f >. e. ( Y N X ) ) )
21 20 eqrelrdv2 
 |-  ( ( ( Rel `' ( X N Y ) /\ Rel ( Y N X ) ) /\ ph ) -> `' ( X N Y ) = ( Y N X ) )
22 12 21 mpancom 
 |-  ( ph -> `' ( X N Y ) = ( Y N X ) )