Metamath Proof Explorer

Theorem oppcval

Description: Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppcval.b 
|- B = ( Base ` C )
oppcval.h 
|- H = ( Hom ` C )
oppcval.x 
|- .x. = ( comp ` C )
oppcval.o 
|- O = ( oppCat ` C )
Assertion oppcval 
|- ( C e. V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )

Proof

Step Hyp Ref Expression
1 oppcval.b 
 |-  B = ( Base ` C )
2 oppcval.h 
 |-  H = ( Hom ` C )
3 oppcval.x 
 |-  .x. = ( comp ` C )
4 oppcval.o 
 |-  O = ( oppCat ` C )
5 elex 
 |-  ( C e. V -> C e. _V )
6 id 
 |-  ( c = C -> c = C )
7 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
8 7 2 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
9 8 tposeqd 
 |-  ( c = C -> tpos ( Hom ` c ) = tpos H )
10 9 opeq2d 
 |-  ( c = C -> <. ( Hom ` ndx ) , tpos ( Hom ` c ) >. = <. ( Hom ` ndx ) , tpos H >. )
11 6 10 oveq12d 
 |-  ( c = C -> ( c sSet <. ( Hom ` ndx ) , tpos ( Hom ` c ) >. ) = ( C sSet <. ( Hom ` ndx ) , tpos H >. ) )
12 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
13 12 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
14 13 sqxpeqd 
 |-  ( c = C -> ( ( Base ` c ) X. ( Base ` c ) ) = ( B X. B ) )
15 fveq2 
 |-  ( c = C -> ( comp ` c ) = ( comp ` C ) )
16 15 3 eqtr4di 
 |-  ( c = C -> ( comp ` c ) = .x. )
17 16 oveqd 
 |-  ( c = C -> ( <. z , ( 2nd ` u ) >. ( comp ` c ) ( 1st ` u ) ) = ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) )
18 17 tposeqd 
 |-  ( c = C -> tpos ( <. z , ( 2nd ` u ) >. ( comp ` c ) ( 1st ` u ) ) = tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) )
19 14 13 18 mpoeq123dv 
 |-  ( c = C -> ( u e. ( ( Base ` c ) X. ( Base ` c ) ) , z e. ( Base ` c ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` c ) ( 1st ` u ) ) ) = ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) )
20 19 opeq2d 
 |-  ( c = C -> <. ( comp ` ndx ) , ( u e. ( ( Base ` c ) X. ( Base ` c ) ) , z e. ( Base ` c ) |-> tpos ( <. z , ( 2nd ` u ) >. ( comp ` c ) ( 1st ` u ) ) ) >. = <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. )
21 11 20 oveq12d 
 |-  ( c = C -> ( ( 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 ) ) ) >. ) = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
22 df-oppc 
 |-  oppCat = ( c e. _V |-> ( ( 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 ) ) ) >. ) )
23 ovex 
 |-  ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) e. _V
24 21 22 23 fvmpt 
 |-  ( C e. _V -> ( oppCat ` C ) = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
25 5 24 syl 
 |-  ( C e. V -> ( oppCat ` C ) = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
26 4 25 syl5eq 
 |-  ( C e. V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos H >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )