Metamath Proof Explorer


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=oppCatC
oppcbas.2 B=BaseC
Assertion oppcbas B=BaseO

Proof

Step Hyp Ref Expression
1 oppcbas.1 O=oppCatC
2 oppcbas.2 B=BaseC
3 baseid Base=SlotBasendx
4 slotsbhcdif BasendxHomndxBasendxcompndxHomndxcompndx
5 4 simp1i BasendxHomndx
6 3 5 setsnid BaseC=BaseCsSetHomndxtposHomC
7 4 simp2i Basendxcompndx
8 3 7 setsnid BaseCsSetHomndxtposHomC=BaseCsSetHomndxtposHomCsSetcompndxuBaseC×BaseC,zBaseCtposz2nducompC1stu
9 6 8 eqtri BaseC=BaseCsSetHomndxtposHomCsSetcompndxuBaseC×BaseC,zBaseCtposz2nducompC1stu
10 eqid BaseC=BaseC
11 eqid HomC=HomC
12 eqid compC=compC
13 10 11 12 1 oppcval CVO=CsSetHomndxtposHomCsSetcompndxuBaseC×BaseC,zBaseCtposz2nducompC1stu
14 13 fveq2d CVBaseO=BaseCsSetHomndxtposHomCsSetcompndxuBaseC×BaseC,zBaseCtposz2nducompC1stu
15 9 14 eqtr4id CVBaseC=BaseO
16 base0 =Base
17 16 eqcomi Base=
18 17 1 fveqprc ¬CVBaseC=BaseO
19 15 18 pm2.61i BaseC=BaseO
20 2 19 eqtri B=BaseO