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

Theorem f1ocnv 5760
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 5616 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5395 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5606 . . . . . . 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 5756 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5756 . 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 1370   `'ccnv 4946   Rel wrel 4952    Fn wfn 5520   -1-1-onto->wf1o 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532
This theorem is referenced by:  f1ocnvb  5761  f1orescnv  5763  f1imacnv  5764  f1cnv  5771  f1ococnv1  5776  f1oresrab  5983  f1ocnvfv2  6092  f1ocnvdm  6097  f1ocnvfvrneq  6098  fcof1o  6105  fveqf1o  6108  isocnv  6129  weniso  6153  f1ofveu  6194  f1oexrnex  6636  fnwelem  6796  oacomf1o  7113  mapsnf1o3  7370  ener  7465  en0  7481  en1  7485  omf1o  7523  domss2  7579  mapen  7584  ssenen  7594  f1fi  7708  f1opwfi  7725  mapfienlem2  7765  mapfienlem3  7766  mapfien  7767  mapfien2  7768  ordiso2  7839  unxpwdom2  7913  cantnfle  7989  cantnfp1lem3  7998  cantnflem1b  8004  cantnflem1d  8006  cantnflem1  8007  cantnfleOLD  8019  cantnfp1lem3OLD  8024  cantnflem1bOLD  8027  cantnflem1dOLD  8029  cantnflem1OLD  8030  mapfienOLD  8037  wemapwe  8038  wemapweOLD  8039  oef1o  8040  oef1oOLD  8041  cnfcomlem  8042  cnfcom  8043  cnfcom2lem  8044  cnfcom2  8045  cnfcom3lem  8046  cnfcom3  8047  cnfcomlemOLD  8050  cnfcomOLD  8051  cnfcom2lemOLD  8052  cnfcom2OLD  8053  cnfcom3lemOLD  8054  cnfcom3OLD  8055  infxpenlem  8290  infxpenc  8294  infxpencOLD  8299  dfac8b  8311  acndom  8331  acndom2  8334  iunfictbso  8394  dfac12lem2  8423  infpssrlem3  8584  infpssrlem4  8585  fin1a2lem7  8685  axcc3  8717  ttukeylem7  8794  fpwwe2lem6  8912  fpwwe2lem7  8913  pwfseqlem5  8940  axdc4uzlem  11920  seqf1olem1  11961  seqf1olem2  11962  hashfacen  12324  seqcoll  12333  seqcoll2  12334  cnrecnv  12771  isercolllem2  13260  isercoll  13262  summolem3  13308  summolem2a  13309  ackbijnn  13408  sadcaddlem  13770  sadadd2lem  13772  sadadd3  13774  sadaddlem  13779  sadasslem  13783  sadeq  13785  phimullem  13971  eulerthlem2  13974  unbenlem  14086  1arith2  14106  xpsbas  14630  xpsadd  14632  xpsmul  14633  xpssca  14634  xpsvsca  14635  xpsless  14636  xpsle  14637  setcinv  15076  catcisolem  15092  xpsmnd  15579  mhmf1o  15591  xpsgrp  15792  ghmf1o  15894  symggrp  16023  symginv  16025  f1omvdcnv  16068  f1omvdconj  16070  pmtrfconj  16090  odngen  16196  gsumval3eu  16501  gsumval3OLD  16502  gsumval3  16505  gsumzf1o  16511  gsumzf1oOLD  16514  lmhmf1o  17249  fidomndrnglem  17500  psrass1lem  17569  coe1sfi  17791  coe1sfiOLD  17792  znleval  18111  zntoslem  18113  znunithash  18121  mdetleib2  18525  basqtop  19415  tgqtop  19416  reghmph  19497  indishmph  19502  cmphaushmeo  19504  ordthmeolem  19505  txhmeo  19507  xpstps  19514  xpstopnlem2  19515  qtopf1  19520  ufldom  19666  symgtgp  19803  tgpconcompeqg  19813  xpsdsfn  20083  xpsxmet  20086  xpsdsval  20087  xpsmet  20088  imasf1obl  20194  xpsxms  20240  xpsms  20241  iccpnfcnv  20647  xrhmeo  20649  ovoliunlem2  21117  vitalilem2  21221  mbfimaopnlem  21265  dvcnvlem  21580  dvcnv  21581  dvcnvrelem2  21622  dvcnvre  21623  efif1olem4  22133  eff1olem  22136  logrn  22142  logf1o  22148  dvlog  22228  asinrebnd  22428  sqff1o  22652  lgsqrlem4  22815  f1otrg  23268  f1otrge  23269  cnvunop  25473  unopadj  25474  fcobij  26175  abliso  26303  tpr2rico  26486  derangenlem  27202  subfacp1lem4  27214  cvmfolem  27311  cvmliftlem6  27322  prodmolem3  27589  prodmolem2a  27590  f1ocan1fv  28767  f1ocan2fv  28768  ismtycnv  28848  ismtyima  28849  ismtyhmeolem  28850  ismtybndlem  28852  rngoisocnv  28934  eldioph2  29247  kelac1  29563  mapfien2OLD  29596  f1oexbi  30303  lautcnv  34057  cdlemk45  34914  cdlemn9  35173
  Copyright terms: Public domain W3C validator