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

Theorem f1ocnv 5648
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 5504 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5283 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5494 . . . . . . 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 569 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 453 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5644 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5644 . 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 1369   `'ccnv 4834   Rel wrel 4840    Fn wfn 5408   -1-1-onto->wf1o 5412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420
This theorem is referenced by:  f1ocnvb  5649  f1orescnv  5651  f1imacnv  5652  f1cnv  5659  f1ococnv1  5664  f1oresrab  5870  f1ocnvfv2  5979  f1ocnvdm  5984  f1ocnvfvrneq  5985  fcof1o  5992  fveqf1o  5995  isocnv  6016  weniso  6040  f1ofveu  6081  f1oexrnex  6522  fnwelem  6682  oacomf1o  6996  mapsnf1o3  7253  ener  7348  en0  7364  en1  7368  omf1o  7406  domss2  7462  mapen  7467  ssenen  7477  f1fi  7590  f1opwfi  7607  mapfienlem2  7647  mapfienlem3  7648  mapfien  7649  mapfien2  7650  ordiso2  7721  unxpwdom2  7795  cantnfle  7871  cantnfp1lem3  7880  cantnflem1b  7886  cantnflem1d  7888  cantnflem1  7889  cantnfleOLD  7901  cantnfp1lem3OLD  7906  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  mapfienOLD  7919  wemapwe  7920  wemapweOLD  7921  oef1o  7922  oef1oOLD  7923  cnfcomlem  7924  cnfcom  7925  cnfcom2lem  7926  cnfcom2  7927  cnfcom3lem  7928  cnfcom3  7929  cnfcomlemOLD  7932  cnfcomOLD  7933  cnfcom2lemOLD  7934  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  infxpenlem  8172  infxpenc  8176  infxpencOLD  8181  dfac8b  8193  acndom  8213  acndom2  8216  iunfictbso  8276  dfac12lem2  8305  infpssrlem3  8466  infpssrlem4  8467  fin1a2lem7  8567  axcc3  8599  ttukeylem7  8676  fpwwe2lem6  8794  fpwwe2lem7  8795  pwfseqlem5  8822  axdc4uzlem  11796  seqf1olem1  11837  seqf1olem2  11838  hashfacen  12199  seqcoll  12208  seqcoll2  12209  cnrecnv  12646  isercolllem2  13135  isercoll  13137  summolem3  13183  summolem2a  13184  ackbijnn  13283  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  sadasslem  13658  sadeq  13660  phimullem  13846  eulerthlem2  13849  unbenlem  13961  1arith2  13981  xpsbas  14504  xpsadd  14506  xpsmul  14507  xpssca  14508  xpsvsca  14509  xpsless  14510  xpsle  14511  setcinv  14950  catcisolem  14966  xpsmnd  15453  xpsgrp  15665  ghmf1o  15767  symggrp  15896  symginv  15898  f1omvdcnv  15941  f1omvdconj  15943  pmtrfconj  15963  odngen  16067  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzf1o  16382  gsumzf1oOLD  16385  lmhmf1o  17107  fidomndrnglem  17358  psrass1lem  17427  coe1sfi  17648  coe1sfiOLD  17649  znleval  17967  zntoslem  17969  znunithash  17977  mdetleib2  18379  basqtop  19264  tgqtop  19265  reghmph  19346  indishmph  19351  cmphaushmeo  19353  ordthmeolem  19354  txhmeo  19356  xpstps  19363  xpstopnlem2  19364  qtopf1  19369  ufldom  19515  symgtgp  19652  tgpconcompeqg  19662  xpsdsfn  19932  xpsxmet  19935  xpsdsval  19936  xpsmet  19937  imasf1obl  20043  xpsxms  20089  xpsms  20090  iccpnfcnv  20496  xrhmeo  20498  ovoliunlem2  20966  vitalilem2  21069  mbfimaopnlem  21113  dvcnvlem  21428  dvcnv  21429  dvcnvrelem2  21470  dvcnvre  21471  efif1olem4  21981  eff1olem  21984  logrn  21990  logf1o  21996  dvlog  22076  asinrebnd  22276  sqff1o  22500  lgsqrlem4  22663  f1otrg  23085  f1otrge  23086  cnvunop  25290  unopadj  25291  fcobij  25993  abliso  26127  tpr2rico  26311  derangenlem  27028  subfacp1lem4  27040  cvmfolem  27137  cvmliftlem6  27148  prodmolem3  27415  prodmolem2a  27416  f1ocan1fv  28591  f1ocan2fv  28592  ismtycnv  28672  ismtyima  28673  ismtyhmeolem  28674  ismtybndlem  28676  rngoisocnv  28758  eldioph2  29071  kelac1  29387  mapfien2OLD  29420  f1oexbi  30127  lautcnv  33627  cdlemk45  34484  cdlemn9  34743
  Copyright terms: Public domain W3C validator