Metamath Proof Explorer

Theorem isinv

Description: Value of the inverse relation. (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 )
invfval.s 
|- S = ( Sect ` C )
Assertion isinv 
|- ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S 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 invfval.s 
 |-  S = ( Sect ` C )
7 1 2 3 4 5 6 invfval 
 |-  ( ph -> ( X N Y ) = ( ( X S Y ) i^i `' ( Y S X ) ) )
8 7 breqd 
 |-  ( ph -> ( F ( X N Y ) G <-> F ( ( X S Y ) i^i `' ( Y S X ) ) G ) )
9 brin 
 |-  ( F ( ( X S Y ) i^i `' ( Y S X ) ) G <-> ( F ( X S Y ) G /\ F `' ( Y S X ) G ) )
10 8 9 bitrdi 
 |-  ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ F `' ( Y S X ) G ) ) )
11 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
12 eqid 
 |-  ( comp ` C ) = ( comp ` C )
13 eqid 
 |-  ( Id ` C ) = ( Id ` C )
14 1 11 12 13 6 3 5 4 sectss 
 |-  ( ph -> ( Y S X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) )
15 relxp 
 |-  Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) )
16 relss 
 |-  ( ( Y S X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> ( Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> Rel ( Y S X ) ) )
17 14 15 16 mpisyl 
 |-  ( ph -> Rel ( Y S X ) )
18 relbrcnvg 
 |-  ( Rel ( Y S X ) -> ( F `' ( Y S X ) G <-> G ( Y S X ) F ) )
19 17 18 syl 
 |-  ( ph -> ( F `' ( Y S X ) G <-> G ( Y S X ) F ) )
20 19 anbi2d 
 |-  ( ph -> ( ( F ( X S Y ) G /\ F `' ( Y S X ) G ) <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) )
21 10 20 bitrd 
 |-  ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) )