Metamath Proof Explorer


Theorem invsym

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 )
invfval.x
|- ( ph -> X e. B )
invfval.y
|- ( ph -> Y e. B )
Assertion invsym
|- ( ph -> ( F ( X N Y ) G <-> G ( Y N X ) F ) )

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 invfval.x
 |-  ( ph -> X e. B )
5 invfval.y
 |-  ( ph -> Y e. B )
6 eqid
 |-  ( Sect ` C ) = ( Sect ` C )
7 1 2 3 4 5 6 isinv
 |-  ( ph -> ( F ( X N Y ) G <-> ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) ) )
8 7 biancomd
 |-  ( ph -> ( F ( X N Y ) G <-> ( G ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) G ) ) )
9 1 2 3 5 4 6 isinv
 |-  ( ph -> ( G ( Y N X ) F <-> ( G ( Y ( Sect ` C ) X ) F /\ F ( X ( Sect ` C ) Y ) G ) ) )
10 8 9 bitr4d
 |-  ( ph -> ( F ( X N Y ) G <-> G ( Y N X ) F ) )