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

Theorem f1ocnv 6047
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 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)

Proof of Theorem f1ocnv
StepHypRef Expression
1 fnrel 5889 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel2 5488 . . . . . 6 (Rel 𝐹𝐹 = 𝐹)
3 fneq1 5879 . . . . . . 7 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
43biimprd 237 . . . . . 6 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
52, 4sylbi 206 . . . . 5 (Rel 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
61, 5mpcom 37 . . . 4 (𝐹 Fn 𝐴𝐹 Fn 𝐴)
76anim2i 591 . . 3 ((𝐹 Fn 𝐵𝐹 Fn 𝐴) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
87ancoms 468 . 2 ((𝐹 Fn 𝐴𝐹 Fn 𝐵) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
9 dff1o4 6043 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
10 dff1o4 6043 . 2 (𝐹:𝐵1-1-onto𝐴 ↔ (𝐹 Fn 𝐵𝐹 Fn 𝐴))
118, 9, 103imtr4i 280 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  ccnv 5027  Rel wrel 5033   Fn wfn 5785  1-1-ontowf1o 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579  df-opab 4639  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797
This theorem is referenced by:  f1ocnvb  6048  f1orescnv  6050  f1imacnv  6051  f1cnv  6058  f1ococnv1  6063  f1oresrab  6287  f1ocnvfv2  6411  f1ocnvdm  6418  f1ocnvfvrneq  6419  fcof1oinvd  6426  fveqf1o  6435  isocnv  6458  weniso  6482  f1ofveu  6522  f1oexrnex  6986  f1oexbi  6987  fnwelem  7157  oacomf1o  7510  mapsnf1o3  7770  ener  7866  enerOLD  7867  en0  7883  en1  7887  omf1o  7926  domss2  7982  mapen  7987  ssenen  7997  f1fi  8114  f1opwfi  8131  mapfienlem2  8172  mapfienlem3  8173  mapfien  8174  mapfien2  8175  ordiso2  8281  unxpwdom2  8354  cantnfle  8429  cantnfp1lem3  8438  cantnflem1b  8444  cantnflem1d  8446  cantnflem1  8447  wemapwe  8455  oef1o  8456  cnfcomlem  8457  cnfcom  8458  cnfcom2lem  8459  cnfcom2  8460  cnfcom3lem  8461  cnfcom3  8462  infxpenlem  8697  infxpenc  8702  dfac8b  8715  acndom  8735  acndom2  8738  iunfictbso  8798  dfac12lem2  8827  infpssrlem3  8988  infpssrlem4  8989  fin1a2lem7  9089  axcc3  9121  ttukeylem7  9198  fpwwe2lem6  9314  fpwwe2lem7  9315  pwfseqlem5  9342  axdc4uzlem  12602  seqf1olem1  12660  seqf1olem2  12661  hashfacen  13050  seqcoll  13060  seqcoll2  13061  cnrecnv  13702  isercolllem2  14193  isercoll  14195  summolem3  14241  summolem2a  14242  ackbijnn  14348  prodmolem3  14451  prodmolem2a  14452  sadcaddlem  14966  sadadd2lem  14968  sadadd3  14970  sadaddlem  14975  sadasslem  14979  sadeq  14981  phimullem  15271  eulerthlem2  15274  unbenlem  15399  1arith2  15419  xpsbas  16006  xpsadd  16008  xpsmul  16009  xpssca  16010  xpsvsca  16011  xpsless  16012  xpsle  16013  setcinv  16512  catcisolem  16528  xpsmnd  17102  mhmf1o  17117  xpsgrp  17306  ghmf1o  17462  symggrp  17592  symginv  17594  f1omvdcnv  17636  f1omvdconj  17638  pmtrfconj  17658  odngen  17764  gsumval3eu  18077  gsumval3  18080  gsumzf1o  18085  lmhmf1o  18816  fidomndrnglem  19076  psrass1lem  19147  coe1sfi  19353  znleval  19670  zntoslem  19672  znunithash  19680  mdetleib2  20161  basqtop  21272  tgqtop  21273  reghmph  21354  indishmph  21359  cmphaushmeo  21361  ordthmeolem  21362  txhmeo  21364  xpstps  21371  xpstopnlem2  21372  qtopf1  21377  ufldom  21524  symgtgp  21663  tgpconcompeqg  21673  xpsdsfn  21940  xpsxmet  21943  xpsdsval  21944  xpsmet  21945  imasf1obl  22051  xpsxms  22097  xpsms  22098  iccpnfcnv  22499  xrhmeo  22501  ovoliunlem2  23023  vitalilem2  23129  mbfimaopnlem  23173  dvcnvlem  23488  dvcnv  23489  dvcnvrelem2  23530  dvcnvre  23531  efif1olem4  24040  eff1olem  24043  logrn  24054  logf1o  24060  dvlog  24142  asinrebnd  24373  sqff1o  24653  lgsqrlem4  24819  cnvmot  25182  f1otrg  25497  f1otrge  25498  cnvunop  27955  unopadj  27956  fresf1o  28609  padct  28679  fcobij  28682  abliso  28821  madjusmdetlem2  29016  madjusmdetlem4  29018  tpr2rico  29080  esumiun  29277  derangenlem  30201  subfacp1lem4  30213  cvmfolem  30309  cvmliftlem6  30320  fv1stcnv  30719  fv2ndcnv  30720  f1ocan1fv  32485  f1ocan2fv  32486  ismtycnv  32565  ismtyima  32566  ismtyhmeolem  32567  ismtybndlem  32569  rngoisocnv  32744  lautcnv  34188  cdlemk45  35047  cdlemn9  35306  eldioph2  36137  kelac1  36445  brco2f1o  37144  brco3f1o  37145  sge0f1o  39069  mgmhmf1o  41569
  Copyright terms: Public domain W3C validator