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

Theorem f1ocnv 5690
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 5546 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5324 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5537 . . . . . . 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 5685 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5685 . 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 4880   Rel wrel 4886    Fn wfn 5452   -1-1-onto->wf1o 5456
This theorem is referenced by:  f1ocnvb  5691  f1orescnv  5693  f1imacnv  5694  f1cnv  5702  f1ococnv1  5707  f1ocnvfv2  6018  f1ocnvdm  6021  f1ocnvfvrneq  6022  fcof1o  6029  fveqf1o  6032  isocnv  6053  weniso  6078  fnwelem  6464  f1ofveu  6587  oacomf1o  6811  mapsnf1o3  7065  ener  7157  en0  7173  en1  7177  omf1o  7214  domss2  7269  mapen  7274  ssenen  7284  f1fi  7396  f1opwfi  7413  ordiso2  7487  unxpwdom2  7559  cantnfle  7629  cantnfp1lem3  7639  cantnflem1b  7645  cantnflem1d  7647  cantnflem1  7648  mapfien  7656  wemapwe  7657  oef1o  7658  cnfcomlem  7659  cnfcom  7660  cnfcom2lem  7661  cnfcom2  7662  cnfcom3lem  7663  cnfcom3  7664  infxpenlem  7900  infxpenc  7904  dfac8b  7917  acndom  7937  acndom2  7940  iunfictbso  8000  dfac12lem2  8029  infpssrlem3  8190  infpssrlem4  8191  fin1a2lem7  8291  axcc3  8323  ttukeylem7  8400  fpwwe2lem6  8515  fpwwe2lem7  8516  pwfseqlem5  8543  axdc4uzlem  11326  seqf1olem1  11367  seqf1olem2  11368  hashfacen  11708  seqcoll  11717  seqcoll2  11718  cnrecnv  11975  isercolllem2  12464  isercoll  12466  summolem3  12513  summolem2a  12514  ackbijnn  12612  sadcaddlem  12974  sadadd2lem  12976  sadadd3  12978  sadaddlem  12983  sadasslem  12987  sadeq  12989  phimullem  13173  eulerthlem2  13176  unbenlem  13281  1arith2  13301  xpsbas  13804  xpsadd  13806  xpsmul  13807  xpssca  13808  xpsvsca  13809  xpsless  13810  xpsle  13811  setcinv  14250  catcisolem  14266  xpsmnd  14740  xpsgrp  14942  ghmf1o  15040  symggrp  15108  symginv  15110  odngen  15216  gsumval3eu  15518  gsumval3  15519  gsumzf1o  15524  lmhmf1o  16127  fidomndrnglem  16371  psrass1lem  16447  coe1sfi  16615  znleval  16840  zntoslem  16842  znunithash  16850  basqtop  17748  tgqtop  17749  reghmph  17830  indishmph  17835  cmphaushmeo  17837  ordthmeolem  17838  txhmeo  17840  xpstps  17847  xpstopnlem2  17848  qtopf1  17853  ufldom  17999  symgtgp  18136  tgpconcompeqg  18146  xpsdsfn  18412  xpsxmet  18415  xpsdsval  18416  xpsmet  18417  imasf1obl  18523  xpsxms  18569  xpsms  18570  iccpnfcnv  18974  xrhmeo  18976  ovoliunlem2  19404  vitalilem2  19506  mbfimaopnlem  19550  dvcnvlem  19865  dvcnv  19866  dvcnvrelem2  19907  dvcnvre  19908  efif1olem4  20452  eff1olem  20455  logrn  20461  logf1o  20467  dvlog  20547  asinrebnd  20746  sqff1o  20970  lgsqrlem4  21133  cnvunop  23426  unopadj  23427  tpr2rico  24315  derangenlem  24862  subfacp1lem4  24874  cvmfolem  24971  cvmliftlem6  24982  prodmolem3  25264  prodmolem2a  25265  f1ocan1fv  26442  f1ocan2fv  26443  ismtycnv  26525  ismtyima  26526  ismtyhmeolem  26527  ismtybndlem  26529  rngoisocnv  26611  eldioph2  26834  kelac1  27152  mapfien2  27249  f1omvdcnv  27378  f1omvdconj  27380  pmtrfconj  27398  lautcnv  30961  cdlemk45  31818  cdlemn9  32077
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 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406
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 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464
  Copyright terms: Public domain W3C validator