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=BaseC
oppcsect.o O=oppCatC
oppcsect.c φCCat
oppcsect.x φXB
oppcsect.y φYB
oppcinv.s I=InvC
oppcinv.t J=InvO
Assertion oppcinv φXJY=YIX

Proof

Step Hyp Ref Expression
1 oppcsect.b B=BaseC
2 oppcsect.o O=oppCatC
3 oppcsect.c φCCat
4 oppcsect.x φXB
5 oppcsect.y φYB
6 oppcinv.s I=InvC
7 oppcinv.t J=InvO
8 incom XSectOYYSectOX-1=YSectOX-1XSectOY
9 eqid SectC=SectC
10 eqid SectO=SectO
11 1 2 3 5 4 9 10 oppcsect2 φYSectOX=YSectCX-1
12 11 cnveqd φYSectOX-1=YSectCX-1-1
13 eqid HomC=HomC
14 eqid compC=compC
15 eqid IdC=IdC
16 1 13 14 15 9 3 5 4 sectss φYSectCXYHomCX×XHomCY
17 relxp RelYHomCX×XHomCY
18 relss YSectCXYHomCX×XHomCYRelYHomCX×XHomCYRelYSectCX
19 16 17 18 mpisyl φRelYSectCX
20 dfrel2 RelYSectCXYSectCX-1-1=YSectCX
21 19 20 sylib φYSectCX-1-1=YSectCX
22 12 21 eqtrd φYSectOX-1=YSectCX
23 1 2 3 4 5 9 10 oppcsect2 φXSectOY=XSectCY-1
24 22 23 ineq12d φYSectOX-1XSectOY=YSectCXXSectCY-1
25 8 24 eqtrid φXSectOYYSectOX-1=YSectCXXSectCY-1
26 2 1 oppcbas B=BaseO
27 2 oppccat CCatOCat
28 3 27 syl φOCat
29 26 7 28 4 5 10 invfval φXJY=XSectOYYSectOX-1
30 1 6 3 5 4 9 invfval φYIX=YSectCXXSectCY-1
31 25 29 30 3eqtr4d φXJY=YIX