Metamath Proof Explorer

Theorem oppcinv

Description: An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses oppcsect.b 
|- B = ( Base ` C )
oppcsect.o 
|- O = ( oppCat ` C )
oppcsect.c 
|- ( ph -> C e. Cat )
oppcsect.x 
|- ( ph -> X e. B )
oppcsect.y 
|- ( ph -> Y e. B )
oppcinv.s 
|- I = ( Inv ` C )
oppcinv.t 
|- J = ( Inv ` O )
Assertion oppcinv 
|- ( ph -> ( X J Y ) = ( Y I X ) )

Proof

Step Hyp Ref Expression
1 oppcsect.b 
 |-  B = ( Base ` C )
2 oppcsect.o 
 |-  O = ( oppCat ` C )
3 oppcsect.c 
 |-  ( ph -> C e. Cat )
4 oppcsect.x 
 |-  ( ph -> X e. B )
5 oppcsect.y 
 |-  ( ph -> Y e. B )
6 oppcinv.s 
 |-  I = ( Inv ` C )
7 oppcinv.t 
 |-  J = ( Inv ` O )
8 incom 
 |-  ( ( X ( Sect ` O ) Y ) i^i `' ( Y ( Sect ` O ) X ) ) = ( `' ( Y ( Sect ` O ) X ) i^i ( X ( Sect ` O ) Y ) )
9 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
10 eqid 
 |-  ( Sect ` O ) = ( Sect ` O )
11 1 2 3 5 4 9 10 oppcsect2 
 |-  ( ph -> ( Y ( Sect ` O ) X ) = `' ( Y ( Sect ` C ) X ) )
12 11 cnveqd 
 |-  ( ph -> `' ( Y ( Sect ` O ) X ) = `' `' ( Y ( Sect ` C ) X ) )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 eqid 
 |-  ( comp ` C ) = ( comp ` C )
15 eqid 
 |-  ( Id ` C ) = ( Id ` C )
16 1 13 14 15 9 3 5 4 sectss 
 |-  ( ph -> ( Y ( Sect ` C ) X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) )
17 relxp 
 |-  Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) )
18 relss 
 |-  ( ( Y ( Sect ` C ) X ) C_ ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> ( Rel ( ( Y ( Hom ` C ) X ) X. ( X ( Hom ` C ) Y ) ) -> Rel ( Y ( Sect ` C ) X ) ) )
19 16 17 18 mpisyl 
 |-  ( ph -> Rel ( Y ( Sect ` C ) X ) )
20 dfrel2 
 |-  ( Rel ( Y ( Sect ` C ) X ) <-> `' `' ( Y ( Sect ` C ) X ) = ( Y ( Sect ` C ) X ) )
21 19 20 sylib 
 |-  ( ph -> `' `' ( Y ( Sect ` C ) X ) = ( Y ( Sect ` C ) X ) )
22 12 21 eqtrd 
 |-  ( ph -> `' ( Y ( Sect ` O ) X ) = ( Y ( Sect ` C ) X ) )
23 1 2 3 4 5 9 10 oppcsect2 
 |-  ( ph -> ( X ( Sect ` O ) Y ) = `' ( X ( Sect ` C ) Y ) )
24 22 23 ineq12d 
 |-  ( ph -> ( `' ( Y ( Sect ` O ) X ) i^i ( X ( Sect ` O ) Y ) ) = ( ( Y ( Sect ` C ) X ) i^i `' ( X ( Sect ` C ) Y ) ) )
25 8 24 syl5eq 
 |-  ( ph -> ( ( X ( Sect ` O ) Y ) i^i `' ( Y ( Sect ` O ) X ) ) = ( ( Y ( Sect ` C ) X ) i^i `' ( X ( Sect ` C ) Y ) ) )
26 2 1 oppcbas 
 |-  B = ( Base ` O )
27 2 oppccat 
 |-  ( C e. Cat -> O e. Cat )
28 3 27 syl 
 |-  ( ph -> O e. Cat )
29 26 7 28 4 5 10 invfval 
 |-  ( ph -> ( X J Y ) = ( ( X ( Sect ` O ) Y ) i^i `' ( Y ( Sect ` O ) X ) ) )
30 1 6 3 5 4 9 invfval 
 |-  ( ph -> ( Y I X ) = ( ( Y ( Sect ` C ) X ) i^i `' ( X ( Sect ` C ) Y ) ) )
31 25 29 30 3eqtr4d 
 |-  ( ph -> ( X J Y ) = ( Y I X ) )