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

Theorem f1ocnv 5736
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  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )

Proof of Theorem f1ocnv
StepHypRef Expression
1 fnrel 5587 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5366 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5577 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 223 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 195 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 36 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 567 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 451 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5732 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5732 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 266 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399   `'ccnv 4912   Rel wrel 4918    Fn wfn 5491   -1-1-onto->wf1o 5495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503
This theorem is referenced by:  f1ocnvb  5737  f1orescnv  5739  f1imacnv  5740  f1cnv  5747  f1ococnv1  5752  f1oresrab  5965  f1ocnvfv2  6084  f1ocnvdm  6089  f1ocnvfvrneq  6090  fcof1oinvd  6097  fveqf1o  6106  isocnv  6127  weniso  6151  f1ofveu  6191  f1oexrnex  6648  f1oexbi  6649  fnwelem  6814  oacomf1o  7132  mapsnf1o3  7386  ener  7481  en0  7497  en1  7501  omf1o  7539  domss2  7595  mapen  7600  ssenen  7610  f1fi  7722  f1opwfi  7739  mapfienlem2  7780  mapfienlem3  7781  mapfien  7782  mapfien2  7783  ordiso2  7855  unxpwdom2  7929  cantnfle  8003  cantnfp1lem3  8012  cantnflem1b  8018  cantnflem1d  8020  cantnflem1  8021  cantnfleOLD  8033  cantnfp1lem3OLD  8038  cantnflem1bOLD  8041  cantnflem1dOLD  8043  cantnflem1OLD  8044  mapfienOLD  8051  wemapwe  8052  wemapweOLD  8053  oef1o  8054  oef1oOLD  8055  cnfcomlem  8056  cnfcom  8057  cnfcom2lem  8058  cnfcom2  8059  cnfcom3lem  8060  cnfcom3  8061  cnfcomlemOLD  8064  cnfcomOLD  8065  cnfcom2lemOLD  8066  cnfcom2OLD  8067  cnfcom3lemOLD  8068  cnfcom3OLD  8069  infxpenlem  8304  infxpenc  8308  infxpencOLD  8313  dfac8b  8325  acndom  8345  acndom2  8348  iunfictbso  8408  dfac12lem2  8437  infpssrlem3  8598  infpssrlem4  8599  fin1a2lem7  8699  axcc3  8731  ttukeylem7  8808  fpwwe2lem6  8924  fpwwe2lem7  8925  pwfseqlem5  8952  axdc4uzlem  11995  seqf1olem1  12049  seqf1olem2  12050  hashfacen  12407  seqcoll  12416  seqcoll2  12417  cnrecnv  13000  isercolllem2  13490  isercoll  13492  summolem3  13538  summolem2a  13539  ackbijnn  13642  prodmolem3  13742  prodmolem2a  13743  sadcaddlem  14109  sadadd2lem  14111  sadadd3  14113  sadaddlem  14118  sadasslem  14122  sadeq  14124  phimullem  14311  eulerthlem2  14314  unbenlem  14428  1arith2  14448  xpsbas  14981  xpsadd  14983  xpsmul  14984  xpssca  14985  xpsvsca  14986  xpsless  14987  xpsle  14988  setcinv  15486  catcisolem  15502  xpsmnd  16077  mhmf1o  16093  xpsgrp  16306  ghmf1o  16413  symggrp  16542  symginv  16544  f1omvdcnv  16586  f1omvdconj  16588  pmtrfconj  16608  odngen  16714  gsumval3eu  17024  gsumval3OLD  17025  gsumval3  17028  gsumzf1o  17034  gsumzf1oOLD  17037  lmhmf1o  17805  fidomndrnglem  18068  psrass1lem  18142  coe1sfi  18365  coe1sfiOLD  18366  znleval  18684  zntoslem  18686  znunithash  18694  mdetleib2  19175  basqtop  20297  tgqtop  20298  reghmph  20379  indishmph  20384  cmphaushmeo  20386  ordthmeolem  20387  txhmeo  20389  xpstps  20396  xpstopnlem2  20397  qtopf1  20402  ufldom  20548  symgtgp  20685  tgpconcompeqg  20695  xpsdsfn  20965  xpsxmet  20968  xpsdsval  20969  xpsmet  20970  imasf1obl  21076  xpsxms  21122  xpsms  21123  iccpnfcnv  21529  xrhmeo  21531  ovoliunlem2  21999  vitalilem2  22103  mbfimaopnlem  22147  dvcnvlem  22462  dvcnv  22463  dvcnvrelem2  22504  dvcnvre  22505  efif1olem4  23017  eff1olem  23020  logrn  23031  logf1o  23037  dvlog  23119  asinrebnd  23348  sqff1o  23573  lgsqrlem4  23736  cnvmot  24048  f1otrg  24295  f1otrge  24296  cnvunop  26953  unopadj  26954  fresf1o  27611  padct  27695  fcobij  27698  abliso  27839  tpr2rico  28048  esumiun  28242  derangenlem  28804  subfacp1lem4  28816  cvmfolem  28913  cvmliftlem6  28924  f1ocan1fv  30383  f1ocan2fv  30384  ismtycnv  30464  ismtyima  30465  ismtyhmeolem  30466  ismtybndlem  30468  rngoisocnv  30550  eldioph2  30860  kelac1  31175  mapfien2OLD  31208  mgmhmf1o  32793  lautcnv  36227  cdlemk45  37086  cdlemn9  37345
  Copyright terms: Public domain W3C validator