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		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4		1re	$$⊢1\in ℝ$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		4nn0	$$⊢4\in {\mathbb{N}}_0$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8		1lt10	$$⊢1<10$$
9	5 6 7 8	declti	$$⊢1<14$$
10	4 9	ltneii	$$⊢1\ne 14$$
11		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
12		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
13	11 12	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 14$$
14	10 13	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
15	3 14	setsnid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(C\right)⟩\right)}$$
16		5nn	$$⊢5\in \mathbb{N}$$
17		4lt5	$$⊢4<5$$
18	7 6 16 17	declt	$$⊢14<15$$
19		4nn	$$⊢4\in \mathbb{N}$$
20	7 19	decnncl	$$⊢14\in \mathbb{N}$$
21	20	nnrei	$$⊢14\in ℝ$$
22	7 16	decnncl	$$⊢15\in \mathbb{N}$$
23	22	nnrei	$$⊢15\in ℝ$$
24	4 21 23	lttri	$$⊢\left(1<14\wedge 14<15\right)\to 1<15$$
25	9 18 24	mp2an	$$⊢1<15$$
26	4 25	ltneii	$$⊢1\ne 15$$
27		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
28	11 27	neeq12i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\leftrightarrow 1\ne 15$$
29	26 28	mpbir	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
30	3 29	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)}$$
31	15 30	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)}$$
32		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
33		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
34		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
35	32 33 34 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)⟩$$
36	35	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)}$$
37	31 36	eqtr4id	$$⊢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$$