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

Theorem f1ocnv 5485
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 5342 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5124 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5333 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 214 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 187 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 32 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 552 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 439 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5480 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5480 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 257 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623   `'ccnv 4688   Rel wrel 4694    Fn wfn 5250   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1ocnvb  5486  f1orescnv  5488  f1imacnv  5489  f1cnv  5497  f1ococnv1  5502  f1ocnvfv2  5793  f1ocnvdm  5796  fcof1o  5803  fveqf1o  5806  isocnv  5827  weniso  5852  fnwelem  6230  f1ofveu  6339  oacomf1o  6563  mapsnf1o3  6816  ener  6908  en0  6924  en1  6928  omf1o  6965  domss2  7020  mapen  7025  ssenen  7035  f1fi  7143  f1opwfi  7159  ordiso2  7230  unxpwdom2  7302  cantnfle  7372  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  mapfien  7399  wemapwe  7400  oef1o  7401  cnfcomlem  7402  cnfcom  7403  cnfcom2lem  7404  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  infxpenlem  7641  infxpenc  7645  dfac8b  7658  acndom  7678  acndom2  7681  iunfictbso  7741  dfac12lem2  7770  infpssrlem3  7931  infpssrlem4  7932  fin1a2lem7  8032  axcc3  8064  ttukeylem7  8142  fpwwe2lem6  8257  fpwwe2lem7  8258  pwfseqlem5  8285  axdc4uzlem  11044  seqf1olem1  11085  seqf1olem2  11086  hashfacen  11392  seqcoll  11401  seqcoll2  11402  cnrecnv  11650  isercolllem2  12139  isercoll  12141  summolem3  12187  summolem2a  12188  ackbijnn  12286  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  phimullem  12847  eulerthlem2  12850  unbenlem  12955  1arith2  12975  xpsbas  13476  xpsadd  13478  xpsmul  13479  xpssca  13480  xpsvsca  13481  xpsless  13482  xpsle  13483  setcinv  13922  catcisolem  13938  xpsmnd  14412  xpsgrp  14614  ghmf1o  14712  symggrp  14780  symginv  14782  odngen  14888  gsumval3eu  15190  gsumval3  15191  gsumzf1o  15196  lmhmf1o  15803  fidomndrnglem  16047  psrass1lem  16123  coe1sfi  16293  znleval  16508  zntoslem  16510  znunithash  16518  basqtop  17402  tgqtop  17403  reghmph  17484  indishmph  17489  cmphaushmeo  17491  ordthmeolem  17492  txhmeo  17494  xpstps  17501  xpstopnlem2  17502  qtopf1  17507  ufldom  17657  symgtgp  17784  tgpconcompeqg  17794  xpsdsfn  17941  xpsxmet  17944  xpsdsval  17945  xpsmet  17946  imasf1obl  18034  xpsxms  18080  xpsms  18081  iccpnfcnv  18442  xrhmeo  18444  ovoliunlem2  18862  vitalilem2  18964  mbfimaopnlem  19010  dvcnvlem  19323  dvcnv  19324  dvcnvrelem2  19365  dvcnvre  19366  efif1olem4  19907  eff1olem  19910  logrn  19916  logf1o  19922  dvlog  19998  asinrebnd  20197  sqff1o  20420  lgsqrlem4  20583  cnvunop  22498  unopadj  22499  tpr2rico  23296  derangenlem  23702  subfacp1lem4  23714  cvmfolem  23810  cvmliftlem6  23821  f2imacnv  25052  f1ofi  25070  domrancur1c  25202  oriso  25214  ltrinvlem  25406  f1ocan1fv  26394  f1ocan2fv  26395  ismtycnv  26526  ismtyima  26527  ismtyhmeolem  26528  ismtybndlem  26530  rngoisocnv  26612  eldioph2  26841  kelac1  27161  mapfien2  27258  f1omvdcnv  27387  f1omvdconj  27389  pmtrfconj  27407  lautcnv  30279  cdlemk45  31136  cdlemn9  31395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262
  Copyright terms: Public domain W3C validator