Theorem oppcbas

Description: Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcbas.2	$$⊢B={\mathrm{Base}}_C$$
Assertion	oppcbas	$$⊢B={\mathrm{Base}}_O$$

Proof

Step	Hyp	Ref	Expression
1		oppcbas.1	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcbas.2	$$⊢B={\mathrm{Base}}_C$$
3		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
4		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
5		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
6	3 4 5 1	oppcval	$$⊢C\in \mathrm{V}\to O=\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)⟩$$
7	6	fveq2d	$$⊢C\in \mathrm{V}\to {\mathrm{Base}}_O={\mathrm{Base}}_{\left(\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)}$$
8		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
9		1re	$$⊢1\in ℝ$$
10		1nn	$$⊢1\in \mathbb{N}$$
11		4nn0	$$⊢4\in {\mathbb{N}}_0$$
12		1nn0	$$⊢1\in {\mathbb{N}}_0$$
13		1lt10	$$⊢1<10$$
14	10 11 12 13	declti	$$⊢1<14$$
15	9 14	ltneii	$$⊢1\ne 14$$
16		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
17		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
18	16 17	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 14$$
19	15 18	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
20	8 19	setsnid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(C\right)⟩\right)}$$
21		5nn	$$⊢5\in \mathbb{N}$$
22		4lt5	$$⊢4<5$$
23	12 11 21 22	declt	$$⊢14<15$$
24		4nn	$$⊢4\in \mathbb{N}$$
25	12 24	decnncl	$$⊢14\in \mathbb{N}$$
26	25	nnrei	$$⊢14\in ℝ$$
27	12 21	decnncl	$$⊢15\in \mathbb{N}$$
28	27	nnrei	$$⊢15\in ℝ$$
29	9 26 28	lttri	$$⊢\left(1<14\wedge 14<15\right)\to 1<15$$
30	14 23 29	mp2an	$$⊢1<15$$
31	9 30	ltneii	$$⊢1\ne 15$$
32		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
33	16 32	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 15$$
34	31 33	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
35	8 34	setsnid	$$⊢{\mathrm{Base}}_{\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(C\right)⟩\right)}={\mathrm{Base}}_{\left(\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)}$$
36	20 35	eqtri	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\left(\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)}$$
37	7 36	syl6reqr	$$⊢C\in \mathrm{V}\to {\mathrm{Base}}_C={\mathrm{Base}}_O$$
38		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
39		fvprc	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Base}}_C=\varnothing$$
40		fvprc	$$⊢\neg C\in \mathrm{V}\to \mathrm{oppCat}\left(C\right)=\varnothing$$
41	1 40	syl5eq	$$⊢\neg C\in \mathrm{V}\to O=\varnothing$$
42	41	fveq2d	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Base}}_O={\mathrm{Base}}_{\varnothing }$$
43	38 39 42	3eqtr4a	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Base}}_C={\mathrm{Base}}_O$$
44	37 43	pm2.61i	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
45	2 44	eqtri	$$⊢B={\mathrm{Base}}_O$$