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

Theorem f1ocnv 5843
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 5692 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5305 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5682 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 226 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 198 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 37 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 571 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 454 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5839 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5839 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 269 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   `'ccnv 4852   Rel wrel 4858    Fn wfn 5596   -1-1-onto->wf1o 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608
This theorem is referenced by:  f1ocnvb  5844  f1orescnv  5846  f1imacnv  5847  f1cnv  5854  f1ococnv1  5859  f1oresrab  6070  f1ocnvfv2  6191  f1ocnvdm  6198  f1ocnvfvrneq  6199  fcof1oinvd  6206  fveqf1o  6215  isocnv  6236  weniso  6260  f1ofveu  6300  f1oexrnex  6756  f1oexbi  6757  fnwelem  6922  oacomf1o  7277  mapsnf1o3  7531  ener  7626  en0  7642  en1  7646  omf1o  7684  domss2  7740  mapen  7745  ssenen  7755  f1fi  7870  f1opwfi  7887  mapfienlem2  7928  mapfienlem3  7929  mapfien  7930  mapfien2  7931  ordiso2  8039  unxpwdom2  8112  cantnfle  8184  cantnfp1lem3  8193  cantnflem1b  8199  cantnflem1d  8201  cantnflem1  8202  wemapwe  8210  oef1o  8211  cnfcomlem  8212  cnfcom  8213  cnfcom2lem  8214  cnfcom2  8215  cnfcom3lem  8216  cnfcom3  8217  infxpenlem  8452  infxpenc  8456  dfac8b  8469  acndom  8489  acndom2  8492  iunfictbso  8552  dfac12lem2  8581  infpssrlem3  8742  infpssrlem4  8743  fin1a2lem7  8843  axcc3  8875  ttukeylem7  8952  fpwwe2lem6  9067  fpwwe2lem7  9068  pwfseqlem5  9095  axdc4uzlem  12201  seqf1olem1  12258  seqf1olem2  12259  hashfacen  12621  seqcoll  12631  seqcoll2  12632  cnrecnv  13228  isercolllem2  13728  isercoll  13730  summolem3  13779  summolem2a  13780  ackbijnn  13885  prodmolem3  13986  prodmolem2a  13987  sadcaddlem  14430  sadadd2lem  14432  sadadd3  14434  sadaddlem  14439  sadasslem  14443  sadeq  14445  phimullem  14726  eulerthlem2  14729  unbenlem  14851  1arith2  14871  xpsbas  15479  xpsadd  15481  xpsmul  15482  xpssca  15483  xpsvsca  15484  xpsless  15485  xpsle  15486  setcinv  15984  catcisolem  16000  xpsmnd  16575  mhmf1o  16591  xpsgrp  16804  ghmf1o  16911  symggrp  17040  symginv  17042  f1omvdcnv  17084  f1omvdconj  17086  pmtrfconj  17106  odngen  17225  gsumval3eu  17537  gsumval3  17540  gsumzf1o  17545  lmhmf1o  18268  fidomndrnglem  18529  psrass1lem  18600  coe1sfi  18805  znleval  19123  zntoslem  19125  znunithash  19133  mdetleib2  19611  basqtop  20724  tgqtop  20725  reghmph  20806  indishmph  20811  cmphaushmeo  20813  ordthmeolem  20814  txhmeo  20816  xpstps  20823  xpstopnlem2  20824  qtopf1  20829  ufldom  20975  symgtgp  21114  tgpconcompeqg  21124  xpsdsfn  21390  xpsxmet  21393  xpsdsval  21394  xpsmet  21395  imasf1obl  21501  xpsxms  21547  xpsms  21548  iccpnfcnv  21970  xrhmeo  21972  ovoliunlem2  22454  vitalilem2  22565  mbfimaopnlem  22609  dvcnvlem  22926  dvcnv  22927  dvcnvrelem2  22968  dvcnvre  22969  efif1olem4  23492  eff1olem  23495  logrn  23506  logf1o  23512  dvlog  23594  asinrebnd  23825  sqff1o  24107  lgsqrlem4  24270  cnvmot  24584  f1otrg  24899  f1otrge  24900  cnvunop  27569  unopadj  27570  fresf1o  28233  padct  28313  fcobij  28316  abliso  28466  madjusmdetlem2  28662  madjusmdetlem4  28664  tpr2rico  28726  esumiun  28923  derangenlem  29902  subfacp1lem4  29914  cvmfolem  30010  cvmliftlem6  30021  fv1stcnv  30429  fv2ndcnv  30430  f1ocan1fv  32017  f1ocan2fv  32018  ismtycnv  32098  ismtyima  32099  ismtyhmeolem  32100  ismtybndlem  32102  rngoisocnv  32184  lautcnv  33624  cdlemk45  34483  cdlemn9  34742  eldioph2  35573  kelac1  35891  sge0f1o  38132  mgmhmf1o  39406
  Copyright terms: Public domain W3C validator