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

Theorem f1ocnv 5818
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 5669 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5447 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5659 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 223 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 195 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 36 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 569 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 453 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5814 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5814 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 266 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383   `'ccnv 4988   Rel wrel 4994    Fn wfn 5573   -1-1-onto->wf1o 5577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585
This theorem is referenced by:  f1ocnvb  5819  f1orescnv  5821  f1imacnv  5822  f1cnv  5829  f1ococnv1  5834  f1oresrab  6048  f1ocnvfv2  6168  f1ocnvdm  6173  f1ocnvfvrneq  6174  fcof1oinvd  6181  fveqf1o  6190  isocnv  6211  weniso  6235  f1ofveu  6276  f1oexrnex  6734  f1oexbi  6735  fnwelem  6900  oacomf1o  7216  mapsnf1o3  7469  ener  7564  en0  7580  en1  7584  omf1o  7622  domss2  7678  mapen  7683  ssenen  7693  f1fi  7809  f1opwfi  7826  mapfienlem2  7867  mapfienlem3  7868  mapfien  7869  mapfien2  7870  ordiso2  7943  unxpwdom2  8017  cantnfle  8093  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1d  8110  cantnflem1  8111  cantnfleOLD  8123  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1dOLD  8133  cantnflem1OLD  8134  mapfienOLD  8141  wemapwe  8142  wemapweOLD  8143  oef1o  8144  oef1oOLD  8145  cnfcomlem  8146  cnfcom  8147  cnfcom2lem  8148  cnfcom2  8149  cnfcom3lem  8150  cnfcom3  8151  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom2lemOLD  8156  cnfcom2OLD  8157  cnfcom3lemOLD  8158  cnfcom3OLD  8159  infxpenlem  8394  infxpenc  8398  infxpencOLD  8403  dfac8b  8415  acndom  8435  acndom2  8438  iunfictbso  8498  dfac12lem2  8527  infpssrlem3  8688  infpssrlem4  8689  fin1a2lem7  8789  axcc3  8821  ttukeylem7  8898  fpwwe2lem6  9016  fpwwe2lem7  9017  pwfseqlem5  9044  axdc4uzlem  12074  seqf1olem1  12128  seqf1olem2  12129  hashfacen  12485  seqcoll  12494  seqcoll2  12495  cnrecnv  12980  isercolllem2  13470  isercoll  13472  summolem3  13518  summolem2a  13519  ackbijnn  13622  prodmolem3  13722  prodmolem2a  13723  sadcaddlem  14089  sadadd2lem  14091  sadadd3  14093  sadaddlem  14098  sadasslem  14102  sadeq  14104  phimullem  14291  eulerthlem2  14294  unbenlem  14408  1arith2  14428  xpsbas  14953  xpsadd  14955  xpsmul  14956  xpssca  14957  xpsvsca  14958  xpsless  14959  xpsle  14960  setcinv  15396  catcisolem  15412  xpsmnd  15939  mhmf1o  15955  xpsgrp  16168  ghmf1o  16275  symggrp  16404  symginv  16406  f1omvdcnv  16448  f1omvdconj  16450  pmtrfconj  16470  odngen  16576  gsumval3eu  16886  gsumval3OLD  16887  gsumval3  16890  gsumzf1o  16896  gsumzf1oOLD  16899  lmhmf1o  17671  fidomndrnglem  17934  psrass1lem  18008  coe1sfi  18231  coe1sfiOLD  18232  znleval  18571  zntoslem  18573  znunithash  18581  mdetleib2  19068  basqtop  20190  tgqtop  20191  reghmph  20272  indishmph  20277  cmphaushmeo  20279  ordthmeolem  20280  txhmeo  20282  xpstps  20289  xpstopnlem2  20290  qtopf1  20295  ufldom  20441  symgtgp  20578  tgpconcompeqg  20588  xpsdsfn  20858  xpsxmet  20861  xpsdsval  20862  xpsmet  20863  imasf1obl  20969  xpsxms  21015  xpsms  21016  iccpnfcnv  21422  xrhmeo  21424  ovoliunlem2  21892  vitalilem2  21996  mbfimaopnlem  22040  dvcnvlem  22355  dvcnv  22356  dvcnvrelem2  22397  dvcnvre  22398  efif1olem4  22910  eff1olem  22913  logrn  22924  logf1o  22930  dvlog  23010  asinrebnd  23210  sqff1o  23434  lgsqrlem4  23597  cnvmot  23906  f1otrg  24152  f1otrge  24153  cnvunop  26815  unopadj  26816  fcobij  27526  abliso  27664  tpr2rico  27872  derangenlem  28593  subfacp1lem4  28605  cvmfolem  28702  cvmliftlem6  28713  f1ocan1fv  30193  f1ocan2fv  30194  ismtycnv  30274  ismtyima  30275  ismtyhmeolem  30276  ismtybndlem  30278  rngoisocnv  30360  eldioph2  30671  kelac1  30985  mapfien2OLD  31018  mgmhmf1o  32429  lautcnv  35689  cdlemk45  36548  cdlemn9  36807
  Copyright terms: Public domain W3C validator