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

Theorem f1ocnv 5654
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 5510 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5288 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5501 . . . . . . 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 5649 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5649 . 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 1649   `'ccnv 4844   Rel wrel 4850    Fn wfn 5416   -1-1-onto->wf1o 5420
This theorem is referenced by:  f1ocnvb  5655  f1orescnv  5657  f1imacnv  5658  f1cnv  5666  f1ococnv1  5671  f1ocnvfv2  5982  f1ocnvdm  5985  f1ocnvfvrneq  5986  fcof1o  5993  fveqf1o  5996  isocnv  6017  weniso  6042  fnwelem  6428  f1ofveu  6551  oacomf1o  6775  mapsnf1o3  7029  ener  7121  en0  7137  en1  7141  omf1o  7178  domss2  7233  mapen  7238  ssenen  7248  f1fi  7360  f1opwfi  7376  ordiso2  7448  unxpwdom2  7520  cantnfle  7590  cantnfp1lem3  7600  cantnflem1b  7606  cantnflem1d  7608  cantnflem1  7609  mapfien  7617  wemapwe  7618  oef1o  7619  cnfcomlem  7620  cnfcom  7621  cnfcom2lem  7622  cnfcom2  7623  cnfcom3lem  7624  cnfcom3  7625  infxpenlem  7859  infxpenc  7863  dfac8b  7876  acndom  7896  acndom2  7899  iunfictbso  7959  dfac12lem2  7988  infpssrlem3  8149  infpssrlem4  8150  fin1a2lem7  8250  axcc3  8282  ttukeylem7  8359  fpwwe2lem6  8474  fpwwe2lem7  8475  pwfseqlem5  8502  axdc4uzlem  11284  seqf1olem1  11325  seqf1olem2  11326  hashfacen  11666  seqcoll  11675  seqcoll2  11676  cnrecnv  11933  isercolllem2  12422  isercoll  12424  summolem3  12471  summolem2a  12472  ackbijnn  12570  sadcaddlem  12932  sadadd2lem  12934  sadadd3  12936  sadaddlem  12941  sadasslem  12945  sadeq  12947  phimullem  13131  eulerthlem2  13134  unbenlem  13239  1arith2  13259  xpsbas  13762  xpsadd  13764  xpsmul  13765  xpssca  13766  xpsvsca  13767  xpsless  13768  xpsle  13769  setcinv  14208  catcisolem  14224  xpsmnd  14698  xpsgrp  14900  ghmf1o  14998  symggrp  15066  symginv  15068  odngen  15174  gsumval3eu  15476  gsumval3  15477  gsumzf1o  15482  lmhmf1o  16085  fidomndrnglem  16329  psrass1lem  16405  coe1sfi  16573  znleval  16798  zntoslem  16800  znunithash  16808  basqtop  17704  tgqtop  17705  reghmph  17786  indishmph  17791  cmphaushmeo  17793  ordthmeolem  17794  txhmeo  17796  xpstps  17803  xpstopnlem2  17804  qtopf1  17809  ufldom  17955  symgtgp  18092  tgpconcompeqg  18102  xpsdsfn  18368  xpsxmet  18371  xpsdsval  18372  xpsmet  18373  imasf1obl  18479  xpsxms  18525  xpsms  18526  iccpnfcnv  18930  xrhmeo  18932  ovoliunlem2  19360  vitalilem2  19462  mbfimaopnlem  19508  dvcnvlem  19821  dvcnv  19822  dvcnvrelem2  19863  dvcnvre  19864  efif1olem4  20408  eff1olem  20411  logrn  20417  logf1o  20423  dvlog  20503  asinrebnd  20702  sqff1o  20926  lgsqrlem4  21089  cnvunop  23382  unopadj  23383  tpr2rico  24271  derangenlem  24818  subfacp1lem4  24830  cvmfolem  24927  cvmliftlem6  24938  prodmolem3  25220  prodmolem2a  25221  f1ocan1fv  26326  f1ocan2fv  26327  ismtycnv  26409  ismtyima  26410  ismtyhmeolem  26411  ismtybndlem  26413  rngoisocnv  26495  eldioph2  26718  kelac1  27037  mapfien2  27134  f1omvdcnv  27263  f1omvdconj  27265  pmtrfconj  27283  lautcnv  30584  cdlemk45  31441  cdlemn9  31700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181  df-opab 4235  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428
  Copyright terms: Public domain W3C validator