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

Theorem f1ocnv 5646
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 5502 . . . . 5  |-  ( F  Fn  A  ->  Rel  F )
2 dfrel2 5280 . . . . . 6  |-  ( Rel 
F  <->  `' `' F  =  F
)
3 fneq1 5493 . . . . . . 7  |-  ( `' `' F  =  F  ->  ( `' `' F  Fn  A  <->  F  Fn  A
) )
43biimprd 215 . . . . . 6  |-  ( `' `' F  =  F  ->  ( F  Fn  A  ->  `' `' F  Fn  A
) )
52, 4sylbi 188 . . . . 5  |-  ( Rel 
F  ->  ( F  Fn  A  ->  `' `' F  Fn  A )
)
61, 5mpcom 34 . . . 4  |-  ( F  Fn  A  ->  `' `' F  Fn  A
)
76anim2i 553 . . 3  |-  ( ( `' F  Fn  B  /\  F  Fn  A
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
87ancoms 440 . 2  |-  ( ( F  Fn  A  /\  `' F  Fn  B
)  ->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
9 dff1o4 5641 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
10 dff1o4 5641 . 2  |-  ( `' F : B -1-1-onto-> A  <->  ( `' F  Fn  B  /\  `' `' F  Fn  A
) )
118, 9, 103imtr4i 258 1  |-  ( F : A -1-1-onto-> B  ->  `' F : B -1-1-onto-> A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649   `'ccnv 4836   Rel wrel 4842    Fn wfn 5408   -1-1-onto->wf1o 5412
This theorem is referenced by:  f1ocnvb  5647  f1orescnv  5649  f1imacnv  5650  f1cnv  5658  f1ococnv1  5663  f1ocnvfv2  5974  f1ocnvdm  5977  f1ocnvfvrneq  5978  fcof1o  5985  fveqf1o  5988  isocnv  6009  weniso  6034  fnwelem  6420  f1ofveu  6543  oacomf1o  6767  mapsnf1o3  7021  ener  7113  en0  7129  en1  7133  omf1o  7170  domss2  7225  mapen  7230  ssenen  7240  f1fi  7352  f1opwfi  7368  ordiso2  7440  unxpwdom2  7512  cantnfle  7582  cantnfp1lem3  7592  cantnflem1b  7598  cantnflem1d  7600  cantnflem1  7601  mapfien  7609  wemapwe  7610  oef1o  7611  cnfcomlem  7612  cnfcom  7613  cnfcom2lem  7614  cnfcom2  7615  cnfcom3lem  7616  cnfcom3  7617  infxpenlem  7851  infxpenc  7855  dfac8b  7868  acndom  7888  acndom2  7891  iunfictbso  7951  dfac12lem2  7980  infpssrlem3  8141  infpssrlem4  8142  fin1a2lem7  8242  axcc3  8274  ttukeylem7  8351  fpwwe2lem6  8466  fpwwe2lem7  8467  pwfseqlem5  8494  axdc4uzlem  11276  seqf1olem1  11317  seqf1olem2  11318  hashfacen  11658  seqcoll  11667  seqcoll2  11668  cnrecnv  11925  isercolllem2  12414  isercoll  12416  summolem3  12463  summolem2a  12464  ackbijnn  12562  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadaddlem  12933  sadasslem  12937  sadeq  12939  phimullem  13123  eulerthlem2  13126  unbenlem  13231  1arith2  13251  xpsbas  13754  xpsadd  13756  xpsmul  13757  xpssca  13758  xpsvsca  13759  xpsless  13760  xpsle  13761  setcinv  14200  catcisolem  14216  xpsmnd  14690  xpsgrp  14892  ghmf1o  14990  symggrp  15058  symginv  15060  odngen  15166  gsumval3eu  15468  gsumval3  15469  gsumzf1o  15474  lmhmf1o  16077  fidomndrnglem  16321  psrass1lem  16397  coe1sfi  16565  znleval  16790  zntoslem  16792  znunithash  16800  basqtop  17696  tgqtop  17697  reghmph  17778  indishmph  17783  cmphaushmeo  17785  ordthmeolem  17786  txhmeo  17788  xpstps  17795  xpstopnlem2  17796  qtopf1  17801  ufldom  17947  symgtgp  18084  tgpconcompeqg  18094  xpsdsfn  18360  xpsxmet  18363  xpsdsval  18364  xpsmet  18365  imasf1obl  18471  xpsxms  18517  xpsms  18518  iccpnfcnv  18922  xrhmeo  18924  ovoliunlem2  19352  vitalilem2  19454  mbfimaopnlem  19500  dvcnvlem  19813  dvcnv  19814  dvcnvrelem2  19855  dvcnvre  19856  efif1olem4  20400  eff1olem  20403  logrn  20409  logf1o  20415  dvlog  20495  asinrebnd  20694  sqff1o  20918  lgsqrlem4  21081  cnvunop  23374  unopadj  23375  tpr2rico  24263  derangenlem  24810  subfacp1lem4  24822  cvmfolem  24919  cvmliftlem6  24930  prodmolem3  25212  prodmolem2a  25213  f1ocan1fv  26318  f1ocan2fv  26319  ismtycnv  26401  ismtyima  26402  ismtyhmeolem  26403  ismtybndlem  26405  rngoisocnv  26487  eldioph2  26710  kelac1  27029  mapfien2  27126  f1omvdcnv  27255  f1omvdconj  27257  pmtrfconj  27275  lautcnv  30572  cdlemk45  31429  cdlemn9  31688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420
  Copyright terms: Public domain W3C validator