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\times {\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	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarf$$
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	$$classtpos\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	$$setvaru$$
15		cbs	$$class\mathrm{Base}$$
16	3 15	cfv	$$class{\mathrm{Base}}_f$$
17	16 16	cxp	$$class\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)$$
18		vz	$$setvarz$$
19	18	cv	$$setvarz$$
20		c2nd	$$class{2}^{nd}$$
21	14	cv	$$setvaru$$
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	$$classtpos\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\times {\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\times {\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\times {\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\times {\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\times {\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)$$