Theorem oppcbas

Description: Base set of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 18-Oct-2024)

	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		slotsbhcdif	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
5	4	simp1i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)$$
6	3 5	setsnid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{\left(C\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),tpos\mathrm{Hom}\left(C\right)⟩\right)}$$
7	4	simp2i	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)$$
8	3 7	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)}$$
9	6 8	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)}$$
10		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
11		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
12		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
13	10 11 12 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)⟩$$
14	13	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)}$$
15	9 14	eqtr4id	$$⊢C\in \mathrm{V}\to {\mathrm{Base}}_C={\mathrm{Base}}_O$$
16		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
17	16	eqcomi	$$⊢{\mathrm{Base}}_{\varnothing }=\varnothing$$
18	17 1	fveqprc	$$⊢\neg C\in \mathrm{V}\to {\mathrm{Base}}_C={\mathrm{Base}}_O$$
19	15 18	pm2.61i	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
20	2 19	eqtri	$$⊢B={\mathrm{Base}}_O$$