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

Theorem f1ocnv 5843
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 5692 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5306 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5682 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 226 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 198 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 37 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 571 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 454 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5839 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5839 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 269 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   `'ccnv 4853   Rel wrel 4859    Fn wfn 5596   -1-1-onto->wf1o 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608
This theorem is referenced by:  f1ocnvb  5844  f1orescnv  5846  f1imacnv  5847  f1cnv  5854  f1ococnv1  5859  f1oresrab  6070  f1ocnvfv2  6191  f1ocnvdm  6198  f1ocnvfvrneq  6199  fcof1oinvd  6206  fveqf1o  6215  isocnv  6236  weniso  6260  f1ofveu  6300  f1oexrnex  6756  f1oexbi  6757  fnwelem  6922  oacomf1o  7274  mapsnf1o3  7528  ener  7623  en0  7639  en1  7643  omf1o  7681  domss2  7737  mapen  7742  ssenen  7752  f1fi  7867  f1opwfi  7884  mapfienlem2  7925  mapfienlem3  7926  mapfien  7927  mapfien2  7928  ordiso2  8030  unxpwdom2  8103  cantnfle  8175  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1d  8192  cantnflem1  8193  wemapwe  8201  oef1o  8202  cnfcomlem  8203  cnfcom  8204  cnfcom2lem  8205  cnfcom2  8206  cnfcom3lem  8207  cnfcom3  8208  infxpenlem  8443  infxpenc  8447  dfac8b  8460  acndom  8480  acndom2  8483  iunfictbso  8543  dfac12lem2  8572  infpssrlem3  8733  infpssrlem4  8734  fin1a2lem7  8834  axcc3  8866  ttukeylem7  8943  fpwwe2lem6  9059  fpwwe2lem7  9060  pwfseqlem5  9087  axdc4uzlem  12192  seqf1olem1  12249  seqf1olem2  12250  hashfacen  12612  seqcoll  12621  seqcoll2  12622  cnrecnv  13207  isercolllem2  13707  isercoll  13709  summolem3  13758  summolem2a  13759  ackbijnn  13864  prodmolem3  13965  prodmolem2a  13966  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadaddlem  14414  sadasslem  14418  sadeq  14420  phimullem  14687  eulerthlem2  14690  unbenlem  14806  1arith2  14826  xpsbas  15422  xpsadd  15424  xpsmul  15425  xpssca  15426  xpsvsca  15427  xpsless  15428  xpsle  15429  setcinv  15927  catcisolem  15943  xpsmnd  16518  mhmf1o  16534  xpsgrp  16747  ghmf1o  16854  symggrp  16983  symginv  16985  f1omvdcnv  17027  f1omvdconj  17029  pmtrfconj  17049  odngen  17155  gsumval3eu  17464  gsumval3  17467  gsumzf1o  17472  lmhmf1o  18195  fidomndrnglem  18456  psrass1lem  18527  coe1sfi  18732  znleval  19047  zntoslem  19049  znunithash  19057  mdetleib2  19535  basqtop  20648  tgqtop  20649  reghmph  20730  indishmph  20735  cmphaushmeo  20737  ordthmeolem  20738  txhmeo  20740  xpstps  20747  xpstopnlem2  20748  qtopf1  20753  ufldom  20899  symgtgp  21038  tgpconcompeqg  21048  xpsdsfn  21314  xpsxmet  21317  xpsdsval  21318  xpsmet  21319  imasf1obl  21425  xpsxms  21471  xpsms  21472  iccpnfcnv  21859  xrhmeo  21861  ovoliunlem2  22325  vitalilem2  22435  mbfimaopnlem  22479  dvcnvlem  22796  dvcnv  22797  dvcnvrelem2  22838  dvcnvre  22839  efif1olem4  23350  eff1olem  23353  logrn  23364  logf1o  23370  dvlog  23452  asinrebnd  23683  sqff1o  23963  lgsqrlem4  24126  cnvmot  24437  f1otrg  24738  f1otrge  24739  cnvunop  27397  unopadj  27398  fresf1o  28062  padct  28141  fcobij  28144  abliso  28288  madjusmdetlem2  28484  madjusmdetlem4  28486  tpr2rico  28548  esumiun  28745  derangenlem  29673  subfacp1lem4  29685  cvmfolem  29781  cvmliftlem6  29792  fv1stcnv  30200  fv2ndcnv  30201  f1ocan1fv  31747  f1ocan2fv  31748  ismtycnv  31828  ismtyima  31829  ismtyhmeolem  31830  ismtybndlem  31832  rngoisocnv  31914  lautcnv  33354  cdlemk45  34213  cdlemn9  34472  eldioph2  35303  kelac1  35617  sge0f1o  37748  mgmhmf1o  38535
  Copyright terms: Public domain W3C validator