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 = ( oppCat ` C )
oppcbas.2 
|- B = ( Base ` C )
Assertion oppcbas 
|- B = ( Base ` O )

Proof

Step Hyp Ref Expression
1 oppcbas.1 
 |-  O = ( oppCat ` C )
2 oppcbas.2 
 |-  B = ( Base ` C )
3 baseid 
 |-  Base = Slot ( Base ` ndx )
4 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
5 4 simp1i 
 |-  ( Base ` ndx ) =/= ( Hom ` ndx )
6 3 5 setsnid 
 |-  ( Base ` C ) = ( Base ` ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) )
7 4 simp2i 
 |-  ( Base ` ndx ) =/= ( comp ` ndx )
8 3 7 setsnid 
 |-  ( Base ` ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) ) = ( Base ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
9 6 8 eqtri 
 |-  ( Base ` C ) = ( Base ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
10 eqid 
 |-  ( Base ` C ) = ( Base ` C )
11 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
12 eqid 
 |-  ( comp ` C ) = ( comp ` C )
13 10 11 12 1 oppcval 
 |-  ( C e. _V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) )
14 13 fveq2d 
 |-  ( C e. _V -> ( Base ` O ) = ( Base ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( ( Base ` C ) X. ( Base ` C ) ) , z e. ( Base ` C ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` C ) ( 1st ` u ) ) ) >. ) ) )
15 9 14 eqtr4id 
 |-  ( C e. _V -> ( Base ` C ) = ( Base ` O ) )
16 base0 
 |-  (/) = ( Base ` (/) )
17 16 eqcomi 
 |-  ( Base ` (/) ) = (/)
18 17 1 fveqprc 
 |-  ( -. C e. _V -> ( Base ` C ) = ( Base ` O ) )
19 15 18 pm2.61i 
 |-  ( Base ` C ) = ( Base ` O )
20 2 19 eqtri 
 |-  B = ( Base ` O )