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

Theorem f1ocnv 5716
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 5572 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5350 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5563 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 216 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 189 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 35 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 554 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 441 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5711 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5711 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 259 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653   `'ccnv 4906   Rel wrel 4912    Fn wfn 5478   -1-1-onto->wf1o 5482
This theorem is referenced by:  f1ocnvb  5717  f1orescnv  5719  f1imacnv  5720  f1cnv  5728  f1ococnv1  5733  f1ocnvfv2  6044  f1ocnvdm  6047  f1ocnvfvrneq  6048  fcof1o  6055  fveqf1o  6058  isocnv  6079  weniso  6104  fnwelem  6490  f1ofveu  6613  oacomf1o  6837  mapsnf1o3  7091  ener  7183  en0  7199  en1  7203  omf1o  7240  domss2  7295  mapen  7300  ssenen  7310  f1fi  7422  f1opwfi  7439  ordiso2  7513  unxpwdom2  7585  cantnfle  7655  cantnfp1lem3  7665  cantnflem1b  7671  cantnflem1d  7673  cantnflem1  7674  mapfien  7682  wemapwe  7683  oef1o  7684  cnfcomlem  7685  cnfcom  7686  cnfcom2lem  7687  cnfcom2  7688  cnfcom3lem  7689  cnfcom3  7690  infxpenlem  7926  infxpenc  7930  dfac8b  7943  acndom  7963  acndom2  7966  iunfictbso  8026  dfac12lem2  8055  infpssrlem3  8216  infpssrlem4  8217  fin1a2lem7  8317  axcc3  8349  ttukeylem7  8426  fpwwe2lem6  8541  fpwwe2lem7  8542  pwfseqlem5  8569  axdc4uzlem  11352  seqf1olem1  11393  seqf1olem2  11394  hashfacen  11734  seqcoll  11743  seqcoll2  11744  cnrecnv  12001  isercolllem2  12490  isercoll  12492  summolem3  12539  summolem2a  12540  ackbijnn  12638  sadcaddlem  13000  sadadd2lem  13002  sadadd3  13004  sadaddlem  13009  sadasslem  13013  sadeq  13015  phimullem  13199  eulerthlem2  13202  unbenlem  13307  1arith2  13327  xpsbas  13830  xpsadd  13832  xpsmul  13833  xpssca  13834  xpsvsca  13835  xpsless  13836  xpsle  13837  setcinv  14276  catcisolem  14292  xpsmnd  14766  xpsgrp  14968  ghmf1o  15066  symggrp  15134  symginv  15136  odngen  15242  gsumval3eu  15544  gsumval3  15545  gsumzf1o  15550  lmhmf1o  16153  fidomndrnglem  16397  psrass1lem  16473  coe1sfi  16641  znleval  16866  zntoslem  16868  znunithash  16876  basqtop  17774  tgqtop  17775  reghmph  17856  indishmph  17861  cmphaushmeo  17863  ordthmeolem  17864  txhmeo  17866  xpstps  17873  xpstopnlem2  17874  qtopf1  17879  ufldom  18025  symgtgp  18162  tgpconcompeqg  18172  xpsdsfn  18438  xpsxmet  18441  xpsdsval  18442  xpsmet  18443  imasf1obl  18549  xpsxms  18595  xpsms  18596  iccpnfcnv  19000  xrhmeo  19002  ovoliunlem2  19430  vitalilem2  19532  mbfimaopnlem  19576  dvcnvlem  19891  dvcnv  19892  dvcnvrelem2  19933  dvcnvre  19934  efif1olem4  20478  eff1olem  20481  logrn  20487  logf1o  20493  dvlog  20573  asinrebnd  20772  sqff1o  20996  lgsqrlem4  21159  cnvunop  23452  unopadj  23453  tpr2rico  24341  derangenlem  24888  subfacp1lem4  24900  cvmfolem  24997  cvmliftlem6  25008  prodmolem3  25290  prodmolem2a  25291  f1ocan1fv  26466  f1ocan2fv  26467  ismtycnv  26549  ismtyima  26550  ismtyhmeolem  26551  ismtybndlem  26553  rngoisocnv  26635  eldioph2  26858  kelac1  27176  mapfien2  27273  f1omvdcnv  27402  f1omvdconj  27404  pmtrfconj  27422  lautcnv  30985  cdlemk45  31842  cdlemn9  32101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pr 4432
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-br 4238  df-opab 4292  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490
  Copyright terms: Public domain W3C validator