Theorem oppchomfval

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

	Ref	Expression
Hypotheses	oppchom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	oppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	oppchomfval	$$⊢tposH=\mathrm{Hom}\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppchom.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
2		oppchom.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
3		homid	$$⊢\mathrm{Hom}=\mathrm{Slot}\mathrm{Hom}\left(\mathrm{ndx}\right)$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		4nn	$$⊢4\in \mathbb{N}$$
6	4 5	decnncl	$$⊢14\in \mathbb{N}$$
7	6	nnrei	$$⊢14\in ℝ$$
8		4nn0	$$⊢4\in {\mathbb{N}}_0$$
9		5nn	$$⊢5\in \mathbb{N}$$
10		4lt5	$$⊢4<5$$
11	4 8 9 10	declt	$$⊢14<15$$
12	7 11	ltneii	$$⊢14\ne 15$$
13		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
14		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
15	13 14	neeq12i	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 14\ne 15$$
16	12 15	mpbir	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
17	3 16	setsnid	$$⊢\mathrm{Hom}\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)=\mathrm{Hom}\left(\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\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)$$
18	1	fvexi	$$⊢H\in \mathrm{V}$$
19	18	tposex	$$⊢tposH\in \mathrm{V}$$
20	3	setsid	$$⊢\left(C\in \mathrm{V}\wedge tposH\in \mathrm{V}\right)\to tposH=\mathrm{Hom}\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)$$
21	19 20	mpan2	$$⊢C\in \mathrm{V}\to tposH=\mathrm{Hom}\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\right)$$
22		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
23		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
24	22 1 23 2	oppcval	$$⊢C\in \mathrm{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({\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)⟩$$
25	24	fveq2d	$$⊢C\in \mathrm{V}\to \mathrm{Hom}\left(O\right)=\mathrm{Hom}\left(\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tposH⟩\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)$$
26	17 21 25	3eqtr4a	$$⊢C\in \mathrm{V}\to tposH=\mathrm{Hom}\left(O\right)$$
27		tpos0	$$⊢tpos\varnothing =\varnothing$$
28		fvprc	$$⊢\neg C\in \mathrm{V}\to \mathrm{Hom}\left(C\right)=\varnothing$$
29	1 28	syl5eq	$$⊢\neg C\in \mathrm{V}\to H=\varnothing$$
30	29	tposeqd	$$⊢\neg C\in \mathrm{V}\to tposH=tpos\varnothing$$
31		fvprc	$$⊢\neg C\in \mathrm{V}\to \mathrm{oppCat}\left(C\right)=\varnothing$$
32	2 31	syl5eq	$$⊢\neg C\in \mathrm{V}\to O=\varnothing$$
33	32	fveq2d	$$⊢\neg C\in \mathrm{V}\to \mathrm{Hom}\left(O\right)=\mathrm{Hom}\left(\varnothing \right)$$
34		df-hom	$$⊢\mathrm{Hom}=\mathrm{Slot}14$$
35	34	str0	$$⊢\varnothing =\mathrm{Hom}\left(\varnothing \right)$$
36	33 35	eqtr4di	$$⊢\neg C\in \mathrm{V}\to \mathrm{Hom}\left(O\right)=\varnothing$$
37	27 30 36	3eqtr4a	$$⊢\neg C\in \mathrm{V}\to tposH=\mathrm{Hom}\left(O\right)$$
38	26 37	pm2.61i	$$⊢tposH=\mathrm{Hom}\left(O\right)$$