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 · ˙ = comp C
oppcco.o O = oppCat C
oppcco.x φ X B
oppcco.y φ Y B
oppcco.z φ Z B
Assertion oppccofval φ X Y comp O Z = tpos Z Y · ˙ X

Proof

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