This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppccofval

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

Ref Expression
Hypotheses oppcco.b 
|- B = ( Base ` C )
oppcco.c 
|- .x. = ( comp ` C )
oppcco.o 
|- O = ( oppCat ` C )
oppcco.x 
|- ( ph -> X e. B )
oppcco.y 
|- ( ph -> Y e. B )
oppcco.z 
|- ( ph -> Z e. B )
Assertion oppccofval 
|- ( ph -> ( <. X , Y >. ( comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )

Proof

Step Hyp Ref Expression
1 oppcco.b 
 |-  B = ( Base ` C )
2 oppcco.c 
 |-  .x. = ( comp ` C )
3 oppcco.o 
 |-  O = ( oppCat ` C )
4 oppcco.x 
 |-  ( ph -> X e. B )
5 oppcco.y 
 |-  ( ph -> Y e. B )
6 oppcco.z 
 |-  ( ph -> Z e. B )
7 elfvex 
 |-  ( X e. ( Base ` C ) -> C e. _V )
8 7 1 eleq2s 
 |-  ( X e. B -> C e. _V )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 1 9 2 3 oppcval 
 |-  ( C e. _V -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
11 4 8 10 3syl 
 |-  ( ph -> O = ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
12 11 fveq2d 
 |-  ( ph -> ( comp ` O ) = ( comp ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) ) )
13 ovex 
 |-  ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) e. _V
14 1 fvexi 
 |-  B e. _V
15 14 14 xpex 
 |-  ( B X. B ) e. _V
16 15 14 mpoex 
 |-  ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) e. _V
17 ccoid 
 |-  comp = Slot ( comp ` ndx )
18 17 setsid 
 |-  ( ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) e. _V /\ ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) e. _V ) -> ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) = ( comp ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) ) )
19 13 16 18 mp2an 
 |-  ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) = ( comp ` ( ( C sSet <. ( Hom ` ndx ) , tpos ( Hom ` C ) >. ) sSet <. ( comp ` ndx ) , ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) >. ) )
20 12 19 eqtr4di 
 |-  ( ph -> ( comp ` O ) = ( u e. ( B X. B ) , z e. B |-> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) ) )
21 simprr 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> z = Z )
22 simprl 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> u = <. X , Y >. )
23 22 fveq2d 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` u ) = ( 2nd ` <. X , Y >. ) )
24 5 adantr 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> Y e. B )
25 op2ndg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 2nd ` <. X , Y >. ) = Y )
26 4 24 25 syl2an2r 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` <. X , Y >. ) = Y )
27 23 26 eqtrd 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 2nd ` u ) = Y )
28 21 27 opeq12d 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> <. z , ( 2nd ` u ) >. = <. Z , Y >. )
29 22 fveq2d 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 1st ` u ) = ( 1st ` <. X , Y >. ) )
30 op1stg 
 |-  ( ( X e. B /\ Y e. B ) -> ( 1st ` <. X , Y >. ) = X )
31 4 24 30 syl2an2r 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 1st ` <. X , Y >. ) = X )
32 29 31 eqtrd 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( 1st ` u ) = X )
33 28 32 oveq12d 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) = ( <. Z , Y >. .x. X ) )
34 33 tposeqd 
 |-  ( ( ph /\ ( u = <. X , Y >. /\ z = Z ) ) -> tpos ( <. z , ( 2nd ` u ) >. .x. ( 1st ` u ) ) = tpos ( <. Z , Y >. .x. X ) )
35 4 5 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
36 ovex 
 |-  ( <. Z , Y >. .x. X ) e. _V
37 36 tposex 
 |-  tpos ( <. Z , Y >. .x. X ) e. _V
38 37 a1i 
 |-  ( ph -> tpos ( <. Z , Y >. .x. X ) e. _V )
39 20 34 35 6 38 ovmpod 
 |-  ( ph -> ( <. X , Y >. ( comp ` O ) Z ) = tpos ( <. Z , Y >. .x. X ) )