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

Theorem f1ocnv 5833
Description: The converse of a one-to-one onto function is also one-to-one onto. (Contributed by NM, 11-Feb-1997.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
f1ocnv

Proof of Theorem f1ocnv
StepHypRef Expression
1 fnrel 5684 . . . . 5
2 dfrel2 5462 . . . . . 6
3 fneq1 5674 . . . . . . 7
43biimprd 223 . . . . . 6
52, 4sylbi 195 . . . . 5
61, 5mpcom 36 . . . 4
76anim2i 569 . . 3
87ancoms 453 . 2
9 dff1o4 5829 . 2
10 dff1o4 5829 . 2
118, 9, 103imtr4i 266 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  `'ccnv 5003  Relwrel 5009  Fnwfn 5588  -1-1-onto->wf1o 5592
This theorem is referenced by:  f1ocnvb  5834  f1orescnv  5836  f1imacnv  5837  f1cnv  5844  f1ococnv1  5849  f1oresrab  6063  f1ocnvfv2  6183  f1ocnvdm  6188  f1ocnvfvrneq  6189  fcof1oinvd  6196  fveqf1o  6205  isocnv  6226  weniso  6250  f1ofveu  6291  f1oexrnex  6749  f1oexbi  6750  fnwelem  6915  oacomf1o  7233  mapsnf1o3  7487  ener  7582  en0  7598  en1  7602  omf1o  7640  domss2  7696  mapen  7701  ssenen  7711  f1fi  7827  f1opwfi  7844  mapfienlem2  7885  mapfienlem3  7886  mapfien  7887  mapfien2  7888  ordiso2  7961  unxpwdom2  8035  cantnfle  8111  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1d  8128  cantnflem1  8129  cantnfleOLD  8141  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1dOLD  8151  cantnflem1OLD  8152  mapfienOLD  8159  wemapwe  8160  wemapweOLD  8161  oef1o  8162  oef1oOLD  8163  cnfcomlem  8164  cnfcom  8165  cnfcom2lem  8166  cnfcom2  8167  cnfcom3lem  8168  cnfcom3  8169  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom2lemOLD  8174  cnfcom2OLD  8175  cnfcom3lemOLD  8176  cnfcom3OLD  8177  infxpenlem  8412  infxpenc  8416  infxpencOLD  8421  dfac8b  8433  acndom  8453  acndom2  8456  iunfictbso  8516  dfac12lem2  8545  infpssrlem3  8706  infpssrlem4  8707  fin1a2lem7  8807  axcc3  8839  ttukeylem7  8916  fpwwe2lem6  9034  fpwwe2lem7  9035  pwfseqlem5  9062  axdc4uzlem  12092  seqf1olem1  12146  seqf1olem2  12147  hashfacen  12503  seqcoll  12512  seqcoll2  12513  cnrecnv  12998  isercolllem2  13488  isercoll  13490  summolem3  13536  summolem2a  13537  ackbijnn  13640  prodmolem3  13740  prodmolem2a  13741  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  sadeq  14122  phimullem  14309  eulerthlem2  14312  unbenlem  14426  1arith2  14446  xpsbas  14971  xpsadd  14973  xpsmul  14974  xpssca  14975  xpsvsca  14976  xpsless  14977  xpsle  14978  setcinv  15417  catcisolem  15433  xpsmnd  15960  mhmf1o  15976  xpsgrp  16189  ghmf1o  16296  symggrp  16425  symginv  16427  f1omvdcnv  16469  f1omvdconj  16471  pmtrfconj  16491  odngen  16597  gsumval3eu  16907  gsumval3OLD  16908  gsumval3  16911  gsumzf1o  16917  gsumzf1oOLD  16920  lmhmf1o  17692  fidomndrnglem  17955  psrass1lem  18029  coe1sfi  18252  coe1sfiOLD  18253  znleval  18593  zntoslem  18595  znunithash  18603  mdetleib2  19090  basqtop  20212  tgqtop  20213  reghmph  20294  indishmph  20299  cmphaushmeo  20301  ordthmeolem  20302  txhmeo  20304  xpstps  20311  xpstopnlem2  20312  qtopf1  20317  ufldom  20463  symgtgp  20600  tgpconcompeqg  20610  xpsdsfn  20880  xpsxmet  20883  xpsdsval  20884  xpsmet  20885  imasf1obl  20991  xpsxms  21037  xpsms  21038  iccpnfcnv  21444  xrhmeo  21446  ovoliunlem2  21914  vitalilem2  22018  mbfimaopnlem  22062  dvcnvlem  22377  dvcnv  22378  dvcnvrelem2  22419  dvcnvre  22420  efif1olem4  22932  eff1olem  22935  logrn  22946  logf1o  22952  dvlog  23032  asinrebnd  23232  sqff1o  23456  lgsqrlem4  23619  cnvmot  23928  f1otrg  24174  f1otrge  24175  cnvunop  26837  unopadj  26838  fcobij  27548  abliso  27686  tpr2rico  27894  derangenlem  28615  subfacp1lem4  28627  cvmfolem  28724  cvmliftlem6  28735  f1ocan1fv  30217  f1ocan2fv  30218  ismtycnv  30298  ismtyima  30299  ismtyhmeolem  30300  ismtybndlem  30302  rngoisocnv  30384  eldioph2  30695  kelac1  31009  mapfien2OLD  31042  mgmhmf1o  32475  lautcnv  35814  cdlemk45  36673  cdlemn9  36932
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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  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-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-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600
  Copyright terms: Public domain W3C validator