Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  oppcval Structured version   Unicode version

Theorem oppcval 15606
 Description: Value of the opposite category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
oppcval.b
oppcval.h
oppcval.x comp
oppcval.o oppCat
Assertion
Ref Expression
oppcval sSet tpos sSet comp tpos
Distinct variable group:   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)

Proof of Theorem oppcval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 oppcval.o . 2 oppCat
2 elex 3090 . . 3
3 id 23 . . . . . 6
4 fveq2 5878 . . . . . . . . 9
5 oppcval.h . . . . . . . . 9
64, 5syl6eqr 2481 . . . . . . . 8
76tposeqd 6981 . . . . . . 7 tpos tpos
87opeq2d 4191 . . . . . 6 tpos tpos
93, 8oveq12d 6320 . . . . 5 sSet tpos sSet tpos
10 fveq2 5878 . . . . . . . . 9
11 oppcval.b . . . . . . . . 9
1210, 11syl6eqr 2481 . . . . . . . 8
1312sqxpeqd 4876 . . . . . . 7
14 fveq2 5878 . . . . . . . . . 10 comp comp
15 oppcval.x . . . . . . . . . 10 comp
1614, 15syl6eqr 2481 . . . . . . . . 9 comp
1716oveqd 6319 . . . . . . . 8 comp
1817tposeqd 6981 . . . . . . 7 tpos comp tpos
1913, 12, 18mpt2eq123dv 6364 . . . . . 6 tpos comp tpos
2019opeq2d 4191 . . . . 5 comp tpos comp comp tpos
219, 20oveq12d 6320 . . . 4 sSet tpos sSet comp tpos comp sSet tpos sSet comp tpos
22 df-oppc 15605 . . . 4 oppCat sSet tpos sSet comp tpos comp
23 ovex 6330 . . . 4 sSet tpos sSet comp tpos
2421, 22, 23fvmpt 5961 . . 3 oppCat sSet tpos sSet comp tpos
252, 24syl 17 . 2 oppCat sSet tpos sSet comp tpos
261, 25syl5eq 2475 1 sSet tpos sSet comp tpos
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wcel 1868  cvv 3081  cop 4002   cxp 4848  cfv 5598  (class class class)co 6302   cmpt2 6304  c1st 6802  c2nd 6803  tpos ctpos 6977  cnx 15106   sSet csts 15107  cbs 15109   chom 15189  compcco 15190  oppCatcoppc 15604 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-res 4862  df-iota 5562  df-fun 5600  df-fv 5606  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-tpos 6978  df-oppc 15605 This theorem is referenced by:  oppchomfval  15607  oppccofval  15609  oppcbas  15611  catcoppccl  15991
 Copyright terms: Public domain W3C validator