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

Theorem f1ocnv 5565
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 5421 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5203 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5412 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 214 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 187 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 32 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 552 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 439 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5560 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5560 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 257 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642   `'ccnv 4767   Rel wrel 4773    Fn wfn 5329   -1-1-onto->wf1o 5333
This theorem is referenced by:  f1ocnvb  5566  f1orescnv  5568  f1imacnv  5569  f1cnv  5577  f1ococnv1  5582  f1ocnvfv2  5877  f1ocnvdm  5880  fcof1o  5887  fveqf1o  5890  isocnv  5911  weniso  5936  fnwelem  6314  f1ofveu  6423  oacomf1o  6647  mapsnf1o3  6901  ener  6993  en0  7009  en1  7013  omf1o  7050  domss2  7105  mapen  7110  ssenen  7120  f1fi  7230  f1opwfi  7246  ordiso2  7317  unxpwdom2  7389  cantnfle  7459  cantnfp1lem3  7469  cantnflem1b  7475  cantnflem1d  7477  cantnflem1  7478  mapfien  7486  wemapwe  7487  oef1o  7488  cnfcomlem  7489  cnfcom  7490  cnfcom2lem  7491  cnfcom2  7492  cnfcom3lem  7493  cnfcom3  7494  infxpenlem  7728  infxpenc  7732  dfac8b  7745  acndom  7765  acndom2  7768  iunfictbso  7828  dfac12lem2  7857  infpssrlem3  8018  infpssrlem4  8019  fin1a2lem7  8119  axcc3  8151  ttukeylem7  8229  fpwwe2lem6  8344  fpwwe2lem7  8345  pwfseqlem5  8372  axdc4uzlem  11133  seqf1olem1  11174  seqf1olem2  11175  hashfacen  11482  seqcoll  11491  seqcoll2  11492  cnrecnv  11740  isercolllem2  12229  isercoll  12231  summolem3  12278  summolem2a  12279  ackbijnn  12377  sadcaddlem  12739  sadadd2lem  12741  sadadd3  12743  sadaddlem  12748  sadasslem  12752  sadeq  12754  phimullem  12938  eulerthlem2  12941  unbenlem  13046  1arith2  13066  xpsbas  13569  xpsadd  13571  xpsmul  13572  xpssca  13573  xpsvsca  13574  xpsless  13575  xpsle  13576  setcinv  14015  catcisolem  14031  xpsmnd  14505  xpsgrp  14707  ghmf1o  14805  symggrp  14873  symginv  14875  odngen  14981  gsumval3eu  15283  gsumval3  15284  gsumzf1o  15289  lmhmf1o  15896  fidomndrnglem  16140  psrass1lem  16216  coe1sfi  16386  znleval  16608  zntoslem  16610  znunithash  16618  basqtop  17502  tgqtop  17503  reghmph  17584  indishmph  17589  cmphaushmeo  17591  ordthmeolem  17592  txhmeo  17594  xpstps  17601  xpstopnlem2  17602  qtopf1  17607  ufldom  17753  symgtgp  17880  tgpconcompeqg  17890  xpsdsfn  18037  xpsxmet  18040  xpsdsval  18041  xpsmet  18042  imasf1obl  18130  xpsxms  18176  xpsms  18177  iccpnfcnv  18540  xrhmeo  18542  ovoliunlem2  18960  vitalilem2  19062  mbfimaopnlem  19108  dvcnvlem  19421  dvcnv  19422  dvcnvrelem2  19463  dvcnvre  19464  efif1olem4  20008  eff1olem  20011  logrn  20017  logf1o  20023  dvlog  20103  asinrebnd  20302  sqff1o  20526  lgsqrlem4  20689  cnvunop  22606  unopadj  22607  tpr2rico  23466  derangenlem  24106  subfacp1lem4  24118  cvmfolem  24214  cvmliftlem6  24225  prodmolem3  24560  prodmolem2a  24561  f1ocan1fv  25718  f1ocan2fv  25719  ismtycnv  25849  ismtyima  25850  ismtyhmeolem  25851  ismtybndlem  25853  rngoisocnv  25935  eldioph2  26164  kelac1  26484  mapfien2  26581  f1omvdcnv  26710  f1omvdconj  26712  pmtrfconj  26730  f1ocnvfvrneq  27423  lautcnv  30331  cdlemk45  31188  cdlemn9  31447
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341
  Copyright terms: Public domain W3C validator