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 · ˙ = comp C
oppcval.o O = oppCat C
Assertion oppcval C V O = C sSet Hom ndx tpos H sSet comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u

Proof

Step Hyp Ref Expression
1 oppcval.b B = Base C
2 oppcval.h H = Hom C
3 oppcval.x · ˙ = comp C
4 oppcval.o O = oppCat C
5 elex C V C 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 × Base c = B × B
15 fveq2 c = C comp c = comp C
16 15 3 eqtr4di c = C comp c = · ˙
17 16 oveqd c = C z 2 nd u comp c 1 st u = z 2 nd u · ˙ 1 st u
18 17 tposeqd c = C tpos z 2 nd u comp c 1 st u = tpos z 2 nd u · ˙ 1 st u
19 14 13 18 mpoeq123dv c = C u Base c × Base c , z Base c tpos z 2 nd u comp c 1 st u = u B × B , z B tpos z 2 nd u · ˙ 1 st u
20 19 opeq2d c = C comp ndx u Base c × Base c , z Base c tpos z 2 nd u comp c 1 st u = comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u
21 11 20 oveq12d c = C c sSet Hom ndx tpos Hom c sSet comp ndx u Base c × Base c , z Base c tpos z 2 nd u comp c 1 st u = C sSet Hom ndx tpos H sSet comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u
22 df-oppc oppCat = c V c sSet Hom ndx tpos Hom c sSet comp ndx u Base c × Base c , z Base c tpos z 2 nd u comp c 1 st u
23 ovex C sSet Hom ndx tpos H sSet comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u V
24 21 22 23 fvmpt C V oppCat C = C sSet Hom ndx tpos H sSet comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u
25 5 24 syl C V oppCat C = C sSet Hom ndx tpos H sSet comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u
26 4 25 eqtrid C V O = C sSet Hom ndx tpos H sSet comp ndx u B × B , z B tpos z 2 nd u · ˙ 1 st u