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

Theorem f1ocnv 5678
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 5534 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5312 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5525 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 215 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 188 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 34 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 553 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 440 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5673 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5673 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 258 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652   `'ccnv 4868   Rel wrel 4874    Fn wfn 5440   -1-1-onto->wf1o 5444
This theorem is referenced by:  f1ocnvb  5679  f1orescnv  5681  f1imacnv  5682  f1cnv  5690  f1ococnv1  5695  f1ocnvfv2  6006  f1ocnvdm  6009  f1ocnvfvrneq  6010  fcof1o  6017  fveqf1o  6020  isocnv  6041  weniso  6066  fnwelem  6452  f1ofveu  6575  oacomf1o  6799  mapsnf1o3  7053  ener  7145  en0  7161  en1  7165  omf1o  7202  domss2  7257  mapen  7262  ssenen  7272  f1fi  7384  f1opwfi  7401  ordiso2  7473  unxpwdom2  7545  cantnfle  7615  cantnfp1lem3  7625  cantnflem1b  7631  cantnflem1d  7633  cantnflem1  7634  mapfien  7642  wemapwe  7643  oef1o  7644  cnfcomlem  7645  cnfcom  7646  cnfcom2lem  7647  cnfcom2  7648  cnfcom3lem  7649  cnfcom3  7650  infxpenlem  7884  infxpenc  7888  dfac8b  7901  acndom  7921  acndom2  7924  iunfictbso  7984  dfac12lem2  8013  infpssrlem3  8174  infpssrlem4  8175  fin1a2lem7  8275  axcc3  8307  ttukeylem7  8384  fpwwe2lem6  8499  fpwwe2lem7  8500  pwfseqlem5  8527  axdc4uzlem  11309  seqf1olem1  11350  seqf1olem2  11351  hashfacen  11691  seqcoll  11700  seqcoll2  11701  cnrecnv  11958  isercolllem2  12447  isercoll  12449  summolem3  12496  summolem2a  12497  ackbijnn  12595  sadcaddlem  12957  sadadd2lem  12959  sadadd3  12961  sadaddlem  12966  sadasslem  12970  sadeq  12972  phimullem  13156  eulerthlem2  13159  unbenlem  13264  1arith2  13284  xpsbas  13787  xpsadd  13789  xpsmul  13790  xpssca  13791  xpsvsca  13792  xpsless  13793  xpsle  13794  setcinv  14233  catcisolem  14249  xpsmnd  14723  xpsgrp  14925  ghmf1o  15023  symggrp  15091  symginv  15093  odngen  15199  gsumval3eu  15501  gsumval3  15502  gsumzf1o  15507  lmhmf1o  16110  fidomndrnglem  16354  psrass1lem  16430  coe1sfi  16598  znleval  16823  zntoslem  16825  znunithash  16833  basqtop  17731  tgqtop  17732  reghmph  17813  indishmph  17818  cmphaushmeo  17820  ordthmeolem  17821  txhmeo  17823  xpstps  17830  xpstopnlem2  17831  qtopf1  17836  ufldom  17982  symgtgp  18119  tgpconcompeqg  18129  xpsdsfn  18395  xpsxmet  18398  xpsdsval  18399  xpsmet  18400  imasf1obl  18506  xpsxms  18552  xpsms  18553  iccpnfcnv  18957  xrhmeo  18959  ovoliunlem2  19387  vitalilem2  19489  mbfimaopnlem  19535  dvcnvlem  19848  dvcnv  19849  dvcnvrelem2  19890  dvcnvre  19891  efif1olem4  20435  eff1olem  20438  logrn  20444  logf1o  20450  dvlog  20530  asinrebnd  20729  sqff1o  20953  lgsqrlem4  21116  cnvunop  23409  unopadj  23410  tpr2rico  24298  derangenlem  24845  subfacp1lem4  24857  cvmfolem  24954  cvmliftlem6  24965  prodmolem3  25248  prodmolem2a  25249  f1ocan1fv  26365  f1ocan2fv  26366  ismtycnv  26448  ismtyima  26449  ismtyhmeolem  26450  ismtybndlem  26452  rngoisocnv  26534  eldioph2  26757  kelac1  27076  mapfien2  27173  f1omvdcnv  27302  f1omvdconj  27304  pmtrfconj  27322  lautcnv  30726  cdlemk45  31583  cdlemn9  31842
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452
  Copyright terms: Public domain W3C validator