Metamath Proof Explorer


Theorem 2oppccomf

Description: The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 O=oppCatC
Assertion 2oppccomf comp𝑓C=comp𝑓oppCatO

Proof

Step Hyp Ref Expression
1 oppcbas.1 O=oppCatC
2 eqid BaseC=BaseC
3 1 2 oppcbas BaseC=BaseO
4 eqid compO=compO
5 eqid oppCatO=oppCatO
6 simpr1 xBaseCyBaseCzBaseCxBaseC
7 simpr2 xBaseCyBaseCzBaseCyBaseC
8 simpr3 xBaseCyBaseCzBaseCzBaseC
9 3 4 5 6 7 8 oppcco xBaseCyBaseCzBaseCgxycompoppCatOzf=fzycompOxg
10 eqid compC=compC
11 2 10 1 8 7 6 oppcco xBaseCyBaseCzBaseCfzycompOxg=gxycompCzf
12 9 11 eqtr2d xBaseCyBaseCzBaseCgxycompCzf=gxycompoppCatOzf
13 12 ralrimivw xBaseCyBaseCzBaseCgyHomCzgxycompCzf=gxycompoppCatOzf
14 13 ralrimivw xBaseCyBaseCzBaseCfxHomCygyHomCzgxycompCzf=gxycompoppCatOzf
15 14 ralrimivvva xBaseCyBaseCzBaseCfxHomCygyHomCzgxycompCzf=gxycompoppCatOzf
16 eqid compoppCatO=compoppCatO
17 eqid HomC=HomC
18 eqidd BaseC=BaseC
19 1 2 2oppcbas BaseC=BaseoppCatO
20 19 a1i BaseC=BaseoppCatO
21 1 2oppchomf Hom𝑓C=Hom𝑓oppCatO
22 21 a1i Hom𝑓C=Hom𝑓oppCatO
23 10 16 17 18 20 22 comfeq comp𝑓C=comp𝑓oppCatOxBaseCyBaseCzBaseCfxHomCygyHomCzgxycompCzf=gxycompoppCatOzf
24 15 23 mpbird comp𝑓C=comp𝑓oppCatO
25 24 mptru comp𝑓C=comp𝑓oppCatO