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

Theorem f1ocnvfv2 6183
Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)
Assertion
Ref Expression
f1ocnvfv2

Proof of Theorem f1ocnvfv2
StepHypRef Expression
1 f1ococnv2 5847 . . . 4
21fveq1d 5873 . . 3
32adantr 465 . 2
4 f1ocnv 5833 . . . 4
5 f1of 5821 . . . 4
64, 5syl 16 . . 3
7 fvco3 5950 . . 3
86, 7sylan 471 . 2
9 fvresi 6097 . . 3
109adantl 466 . 2
113, 8, 103eqtr3d 2506 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818   cid 4795  `'ccnv 5003  |`cres 5006  o.ccom 5008  -->wf 5589  -1-1-onto->wf1o 5592  `cfv 5593
This theorem is referenced by:  f1ocnvfvb  6185  fveqf1o  6205  isocnv  6226  f1oiso2  6248  weniso  6250  ordiso2  7961  cantnfle  8111  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1d  8128  cantnflem1  8129  cantnfleOLD  8141  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1dOLD  8151  cantnflem1OLD  8152  cnfcom2lem  8166  cnfcom2  8167  cnfcom3lem  8168  cnfcom2lemOLD  8174  cnfcom2OLD  8175  cnfcom3lemOLD  8176  acndom2  8456  iunfictbso  8516  ttukeylem7  8916  fpwwe2lem6  9034  fpwwe2lem7  9035  uzrdglem  12068  uzrdgsuci  12071  fzennn  12078  axdc4uzlem  12092  seqf1olem1  12146  seqf1olem2  12147  hashfz1  12419  seqcoll  12512  seqcoll2  12513  summolem3  13536  summolem2a  13537  ackbijnn  13640  prodmolem3  13740  prodmolem2a  13741  sadcaddlem  14107  sadaddlem  14116  sadasslem  14120  sadeq  14122  phimullem  14309  eulerthlem2  14312  catcisolem  15433  mhmf1o  15976  ghmf1o  16296  f1omvdconj  16471  gsumval3eu  16907  gsumval3OLD  16908  gsumval3  16911  lmhmf1o  17692  fidomndrnglem  17955  basqtop  20212  tgqtop  20213  ordthmeolem  20302  symgtgp  20600  imasf1obl  20991  xrhmeo  21446  ovoliunlem2  21914  vitalilem2  22018  dvcnvlem  22377  dvcnv  22378  dvcnvre  22420  efif1olem4  22932  eff1olem  22935  eflog  22964  dvrelog  23018  dvlog  23032  asinrebnd  23232  sqff1o  23456  lgsqrlem4  23619  cnvmot  23928  f1otrg  24174  f1otrge  24175  axcontlem10  24276  nbgracnvfv  24440  cusgrares  24472  usgra2adedgspthlem1  24611  constr3trllem5  24654  cusconngra  24676  wlkiswwlk2lem4  24694  clwlkisclwwlklem2a4  24784  2pthfrgra  25011  cnvunop  26837  unopadj  26838  bracnvbra  27032  abliso  27686  mndpluscn  27908  cvmfolem  28724  cvmliftlem6  28735  f1ocan1fv  30217  ismtycnv  30298  ismtyima  30299  ismtybndlem  30302  rngoisocnv  30384  rmxyval  30851  usgra2adedglem1  32356  mgmhmf1o  32475  lautcnvle  35813  lautcvr  35816  lautj  35817  lautm  35818  ltrncnvatb  35862  ltrncnvel  35866  ltrncnv  35870  ltrneq2  35872  cdlemg17h  36394  diainN  36784  diasslssN  36786  doca3N  36854  dihcnvid2  37000  dochocss  37093  mapdcnvid2  37384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601
  Copyright terms: Public domain W3C validator