# Metamath Proof Explorer

## Definition df-oppc

Description: Define an opposite category, which is the same as the original category but with the direction of arrows the other way around. Definition 3.5 of Adamek p. 25. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-oppc ${⊢}\mathrm{oppCat}=\left({f}\in \mathrm{V}⟼\left({f}\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left({f}\right)⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({u}\in \left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right),{z}\in {\mathrm{Base}}_{{f}}⟼tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)\right)⟩\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 coppc ${class}\mathrm{oppCat}$
1 vf ${setvar}{f}$
2 cvv ${class}\mathrm{V}$
3 1 cv ${setvar}{f}$
4 csts ${class}\mathrm{sSet}$
5 chom ${class}\mathrm{Hom}$
6 cnx ${class}\mathrm{ndx}$
7 6 5 cfv ${class}\mathrm{Hom}\left(\mathrm{ndx}\right)$
8 3 5 cfv ${class}\mathrm{Hom}\left({f}\right)$
9 8 ctpos ${class}tpos\mathrm{Hom}\left({f}\right)$
10 7 9 cop ${class}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left({f}\right)⟩$
11 3 10 4 co ${class}\left({f}\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left({f}\right)⟩\right)$
12 cco ${class}\mathrm{comp}$
13 6 12 cfv ${class}\mathrm{comp}\left(\mathrm{ndx}\right)$
14 vu ${setvar}{u}$
15 cbs ${class}\mathrm{Base}$
16 3 15 cfv ${class}{\mathrm{Base}}_{{f}}$
17 16 16 cxp ${class}\left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right)$
18 vz ${setvar}{z}$
19 18 cv ${setvar}{z}$
20 c2nd ${class}{2}^{nd}$
21 14 cv ${setvar}{u}$
22 21 20 cfv ${class}{2}^{nd}\left({u}\right)$
23 19 22 cop ${class}⟨{z},{2}^{nd}\left({u}\right)⟩$
24 3 12 cfv ${class}\mathrm{comp}\left({f}\right)$
25 c1st ${class}{1}^{st}$
26 21 25 cfv ${class}{1}^{st}\left({u}\right)$
27 23 26 24 co ${class}\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)$
28 27 ctpos ${class}tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)$
29 14 18 17 16 28 cmpo ${class}\left({u}\in \left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right),{z}\in {\mathrm{Base}}_{{f}}⟼tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)\right)$
30 13 29 cop ${class}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({u}\in \left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right),{z}\in {\mathrm{Base}}_{{f}}⟼tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)\right)⟩$
31 11 30 4 co ${class}\left(\left({f}\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left({f}\right)⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({u}\in \left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right),{z}\in {\mathrm{Base}}_{{f}}⟼tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)\right)⟩\right)$
32 1 2 31 cmpt ${class}\left({f}\in \mathrm{V}⟼\left({f}\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left({f}\right)⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({u}\in \left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right),{z}\in {\mathrm{Base}}_{{f}}⟼tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)\right)⟩\right)$
33 0 32 wceq ${wff}\mathrm{oppCat}=\left({f}\in \mathrm{V}⟼\left({f}\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left({f}\right)⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({u}\in \left({\mathrm{Base}}_{{f}}×{\mathrm{Base}}_{{f}}\right),{z}\in {\mathrm{Base}}_{{f}}⟼tpos\left(⟨{z},{2}^{nd}\left({u}\right)⟩\mathrm{comp}\left({f}\right){1}^{st}\left({u}\right)\right)\right)⟩\right)$