Metamath Proof Explorer


Theorem oppcsect

Description: A section 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
oppcsect.s S=SectC
oppcsect.t T=SectO
Assertion oppcsect φFXTYGGXSYF

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 oppcsect.s S=SectC
7 oppcsect.t T=SectO
8 eqid compC=compC
9 4 adantr φGXHomCYFYHomCXXB
10 5 adantr φGXHomCYFYHomCXYB
11 1 8 2 9 10 9 oppcco φGXHomCYFYHomCXGXYcompOXF=FXYcompCXG
12 3 adantr φGXHomCYFYHomCXCCat
13 eqid IdC=IdC
14 2 13 oppcid CCatIdO=IdC
15 12 14 syl φGXHomCYFYHomCXIdO=IdC
16 15 fveq1d φGXHomCYFYHomCXIdOX=IdCX
17 11 16 eqeq12d φGXHomCYFYHomCXGXYcompOXF=IdOXFXYcompCXG=IdCX
18 17 pm5.32da φGXHomCYFYHomCXGXYcompOXF=IdOXGXHomCYFYHomCXFXYcompCXG=IdCX
19 df-3an FXHomOYGYHomOXGXYcompOXF=IdOXFXHomOYGYHomOXGXYcompOXF=IdOX
20 eqid HomC=HomC
21 20 2 oppchom XHomOY=YHomCX
22 21 eleq2i FXHomOYFYHomCX
23 20 2 oppchom YHomOX=XHomCY
24 23 eleq2i GYHomOXGXHomCY
25 22 24 anbi12ci FXHomOYGYHomOXGXHomCYFYHomCX
26 25 anbi1i FXHomOYGYHomOXGXYcompOXF=IdOXGXHomCYFYHomCXGXYcompOXF=IdOX
27 19 26 bitri FXHomOYGYHomOXGXYcompOXF=IdOXGXHomCYFYHomCXGXYcompOXF=IdOX
28 df-3an GXHomCYFYHomCXFXYcompCXG=IdCXGXHomCYFYHomCXFXYcompCXG=IdCX
29 18 27 28 3bitr4g φFXHomOYGYHomOXGXYcompOXF=IdOXGXHomCYFYHomCXFXYcompCXG=IdCX
30 2 1 oppcbas B=BaseO
31 eqid HomO=HomO
32 eqid compO=compO
33 eqid IdO=IdO
34 2 oppccat CCatOCat
35 3 34 syl φOCat
36 30 31 32 33 7 35 4 5 issect φFXTYGFXHomOYGYHomOXGXYcompOXF=IdOX
37 1 20 8 13 6 3 4 5 issect φGXSYFGXHomCYFYHomCXFXYcompCXG=IdCX
38 29 36 37 3bitr4d φFXTYGGXSYF