Theorem oppcval

Description: Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcval.b	$$⊢B={\mathrm{Base}}_C$$
	oppcval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	oppcval.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
	oppcval.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	oppcval	$$⊢C\in V\to O=\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		oppcval.b	$$⊢B={\mathrm{Base}}_C$$
2		oppcval.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
3		oppcval.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
4		oppcval.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
5		elex	$$⊢C\in V\to C\in \mathrm{V}$$
6		id	$$⊢c=C\to c=C$$
7		fveq2	$$⊢c=C\to \mathrm{Hom}\left(c\right)=\mathrm{Hom}\left(C\right)$$
8	7 2	eqtr4di	$$⊢c=C\to \mathrm{Hom}\left(c\right)=H$$
9	8	tposeqd	$$⊢c=C\to tpos\mathrm{Hom}\left(c\right)=tposH$$
10	9	opeq2d	$$⊢c=C\to ⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(c\right)⟩=⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩$$
11	6 10	oveq12d	$$⊢c=C\to c\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(c\right)⟩=C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩$$
12		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
13	12 1	eqtr4di	$$⊢c=C\to {\mathrm{Base}}_c=B$$
14	13	sqxpeqd	$$⊢c=C\to {\mathrm{Base}}_c\times {\mathrm{Base}}_c=B\times B$$
15		fveq2	$$⊢c=C\to \mathrm{comp}\left(c\right)=\mathrm{comp}\left(C\right)$$
16	15 3	eqtr4di	$$⊢c=C\to \mathrm{comp}\left(c\right)=\underset{\dot{}}{·}$$
17	16	oveqd	$$⊢c=C\to ⟨z,2^{nd}\left(u\right)⟩\mathrm{comp}\left(c\right)1^{st}\left(u\right)=⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)$$
18	17	tposeqd	$$⊢c=C\to tpos\left(⟨z,2^{nd}\left(u\right)⟩\mathrm{comp}\left(c\right)1^{st}\left(u\right)\right)=tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)$$
19	14 13 18	mpoeq123dv	$$⊢c=C\to \left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),z\in {\mathrm{Base}}_c⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\mathrm{comp}\left(c\right)1^{st}\left(u\right)\right)\right)=\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)$$
20	19	opeq2d	$$⊢c=C\to ⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),z\in {\mathrm{Base}}_c⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\mathrm{comp}\left(c\right)1^{st}\left(u\right)\right)\right)⟩=⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩$$
21	11 20	oveq12d	$$⊢c=C\to \left(c\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(c\right)⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),z\in {\mathrm{Base}}_c⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\mathrm{comp}\left(c\right)1^{st}\left(u\right)\right)\right)⟩=\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩$$
22		df-oppc	$$⊢\mathrm{oppCat}=\left(c\in \mathrm{V}⟼\left(c\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(c\right)⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right),z\in {\mathrm{Base}}_c⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\mathrm{comp}\left(c\right)1^{st}\left(u\right)\right)\right)⟩\right)$$
23		ovex	$$⊢\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩\in \mathrm{V}$$
24	21 22 23	fvmpt	$$⊢C\in \mathrm{V}\to \mathrm{oppCat}\left(C\right)=\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩$$
25	5 24	syl	$$⊢C\in V\to \mathrm{oppCat}\left(C\right)=\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩$$
26	4 25	eqtrid	$$⊢C\in V\to O=\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(u\in \left(B\times B\right),z\in B⟼tpos\left(⟨z,2^{nd}\left(u\right)⟩\underset{\dot{}}{·}{1}^{st}\left(u\right)\right)\right)⟩$$