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

Theorem f1ocnv 5641
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 5497 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5276 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5487 . . . . . . 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 564 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 450 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5637 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5637 . 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 369    = wceq 1362   `'ccnv 4826   Rel wrel 4832    Fn wfn 5401   -1-1-onto->wf1o 5405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413
This theorem is referenced by:  f1ocnvb  5642  f1orescnv  5644  f1imacnv  5645  f1cnv  5652  f1ococnv1  5657  f1oresrab  5862  f1ocnvfv2  5971  f1ocnvdm  5976  f1ocnvfvrneq  5977  fcof1o  5984  fveqf1o  5987  isocnv  6008  weniso  6032  f1ofveu  6074  f1oexrnex  6516  fnwelem  6676  oacomf1o  6992  mapsnf1o3  7249  ener  7344  en0  7360  en1  7364  omf1o  7402  domss2  7458  mapen  7463  ssenen  7473  f1fi  7586  f1opwfi  7603  mapfienlem2  7643  mapfienlem3  7644  mapfien  7645  mapfien2  7646  ordiso2  7717  unxpwdom2  7791  cantnfle  7867  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1d  7884  cantnflem1  7885  cantnfleOLD  7897  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1dOLD  7907  cantnflem1OLD  7908  mapfienOLD  7915  wemapwe  7916  wemapweOLD  7917  oef1o  7918  oef1oOLD  7919  cnfcomlem  7920  cnfcom  7921  cnfcom2lem  7922  cnfcom2  7923  cnfcom3lem  7924  cnfcom3  7925  cnfcomlemOLD  7928  cnfcomOLD  7929  cnfcom2lemOLD  7930  cnfcom2OLD  7931  cnfcom3lemOLD  7932  cnfcom3OLD  7933  infxpenlem  8168  infxpenc  8172  infxpencOLD  8177  dfac8b  8189  acndom  8209  acndom2  8212  iunfictbso  8272  dfac12lem2  8301  infpssrlem3  8462  infpssrlem4  8463  fin1a2lem7  8563  axcc3  8595  ttukeylem7  8672  fpwwe2lem6  8790  fpwwe2lem7  8791  pwfseqlem5  8818  axdc4uzlem  11788  seqf1olem1  11829  seqf1olem2  11830  hashfacen  12191  seqcoll  12200  seqcoll2  12201  cnrecnv  12638  isercolllem2  13127  isercoll  13129  summolem3  13175  summolem2a  13176  ackbijnn  13274  sadcaddlem  13636  sadadd2lem  13638  sadadd3  13640  sadaddlem  13645  sadasslem  13649  sadeq  13651  phimullem  13837  eulerthlem2  13840  unbenlem  13952  1arith2  13972  xpsbas  14495  xpsadd  14497  xpsmul  14498  xpssca  14499  xpsvsca  14500  xpsless  14501  xpsle  14502  setcinv  14941  catcisolem  14957  xpsmnd  15444  xpsgrp  15654  ghmf1o  15756  symggrp  15885  symginv  15887  f1omvdcnv  15930  f1omvdconj  15932  pmtrfconj  15952  odngen  16056  gsumval3eu  16361  gsumval3OLD  16362  gsumval3  16365  gsumzf1o  16371  gsumzf1oOLD  16374  lmhmf1o  17049  fidomndrnglem  17300  psrass1lem  17381  coe1sfi  17567  coe1sfiOLD  17568  znleval  17829  zntoslem  17831  znunithash  17839  mdetleib2  18241  basqtop  19126  tgqtop  19127  reghmph  19208  indishmph  19213  cmphaushmeo  19215  ordthmeolem  19216  txhmeo  19218  xpstps  19225  xpstopnlem2  19226  qtopf1  19231  ufldom  19377  symgtgp  19514  tgpconcompeqg  19524  xpsdsfn  19794  xpsxmet  19797  xpsdsval  19798  xpsmet  19799  imasf1obl  19905  xpsxms  19951  xpsms  19952  iccpnfcnv  20358  xrhmeo  20360  ovoliunlem2  20828  vitalilem2  20931  mbfimaopnlem  20975  dvcnvlem  21290  dvcnv  21291  dvcnvrelem2  21332  dvcnvre  21333  efif1olem4  21886  eff1olem  21889  logrn  21895  logf1o  21901  dvlog  21981  asinrebnd  22181  sqff1o  22405  lgsqrlem4  22568  f1otrg  22940  f1otrge  22941  cnvunop  25145  unopadj  25146  fcobij  25849  abliso  25983  tpr2rico  26196  derangenlem  26907  subfacp1lem4  26919  cvmfolem  27016  cvmliftlem6  27027  prodmolem3  27293  prodmolem2a  27294  f1ocan1fv  28464  f1ocan2fv  28465  ismtycnv  28545  ismtyima  28546  ismtyhmeolem  28547  ismtybndlem  28549  rngoisocnv  28631  eldioph2  28945  kelac1  29261  mapfien2OLD  29294  f1oexbi  30002  lautcnv  33307  cdlemk45  34164  cdlemn9  34423
  Copyright terms: Public domain W3C validator