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

Theorem f1ocnv 6187
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 6027 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel2 5618 . . . . . 6 (Rel 𝐹𝐹 = 𝐹)
3 fneq1 6017 . . . . . . 7 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
43biimprd 238 . . . . . 6 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
52, 4sylbi 207 . . . . 5 (Rel 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
61, 5mpcom 38 . . . 4 (𝐹 Fn 𝐴𝐹 Fn 𝐴)
76anim2i 592 . . 3 ((𝐹 Fn 𝐵𝐹 Fn 𝐴) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
87ancoms 468 . 2 ((𝐹 Fn 𝐴𝐹 Fn 𝐵) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
9 dff1o4 6183 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
10 dff1o4 6183 . 2 (𝐹:𝐵1-1-onto𝐴 ↔ (𝐹 Fn 𝐵𝐹 Fn 𝐴))
118, 9, 103imtr4i 281 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  ccnv 5142  Rel wrel 5148   Fn wfn 5921  1-1-ontowf1o 5925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933
This theorem is referenced by:  f1ocnvb  6188  f1orescnv  6190  f1imacnv  6191  f1cnv  6198  f1ococnv1  6203  f1oresrab  6435  f1ocnvfv2  6573  f1ocnvdm  6580  f1ocnvfvrneq  6581  fcof1oinvd  6588  fveqf1o  6597  isocnv  6620  weniso  6644  f1ofveu  6685  f1oexrnex  7157  f1oexbi  7158  fnwelem  7337  oacomf1o  7690  mapsnf1o3  7948  ener  8044  en0  8060  en1  8064  omf1o  8104  domss2  8160  mapen  8165  ssenen  8175  f1fi  8294  f1opwfi  8311  mapfienlem2  8352  mapfienlem3  8353  mapfien  8354  mapfien2  8355  ordiso2  8461  unxpwdom2  8534  cantnfle  8606  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1d  8623  cantnflem1  8624  wemapwe  8632  oef1o  8633  cnfcomlem  8634  cnfcom  8635  cnfcom2lem  8636  cnfcom2  8637  cnfcom3lem  8638  cnfcom3  8639  infxpenlem  8874  infxpenc  8879  dfac8b  8892  acndom  8912  acndom2  8915  iunfictbso  8975  dfac12lem2  9004  infpssrlem3  9165  infpssrlem4  9166  fin1a2lem7  9266  axcc3  9298  ttukeylem7  9375  fpwwe2lem6  9495  fpwwe2lem7  9496  pwfseqlem5  9523  axdc4uzlem  12822  seqf1olem1  12880  seqf1olem2  12881  hashfacen  13276  seqcoll  13286  seqcoll2  13287  cnrecnv  13949  isercolllem2  14440  isercoll  14442  summolem3  14489  summolem2a  14490  ackbijnn  14604  prodmolem3  14707  prodmolem2a  14708  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadaddlem  15235  sadasslem  15239  sadeq  15241  phimullem  15531  eulerthlem2  15534  unbenlem  15659  1arith2  15679  xpsbas  16281  xpsadd  16283  xpsmul  16284  xpssca  16285  xpsvsca  16286  xpsless  16287  xpsle  16288  setcinv  16787  catcisolem  16803  xpsmnd  17377  mhmf1o  17392  xpsgrp  17581  ghmf1o  17737  symggrp  17866  symginv  17868  f1omvdcnv  17910  f1omvdconj  17912  pmtrfconj  17932  odngen  18038  gsumval3eu  18351  gsumval3  18354  gsumzf1o  18359  lmhmf1o  19094  fidomndrnglem  19354  psrass1lem  19425  coe1sfi  19631  znleval  19951  zntoslem  19953  znunithash  19961  mdetleib2  20442  basqtop  21562  tgqtop  21563  reghmph  21644  indishmph  21649  cmphaushmeo  21651  ordthmeolem  21652  txhmeo  21654  xpstps  21661  xpstopnlem2  21662  qtopf1  21667  ufldom  21813  symgtgp  21952  tgpconncompeqg  21962  xpsdsfn  22229  xpsxmet  22232  xpsdsval  22233  xpsmet  22234  imasf1obl  22340  xpsxms  22386  xpsms  22387  iccpnfcnv  22790  xrhmeo  22792  ovoliunlem2  23317  vitalilem2  23423  mbfimaopnlem  23467  dvcnvlem  23784  dvcnv  23785  dvcnvrelem2  23826  dvcnvre  23827  efif1olem4  24336  eff1olem  24339  logrn  24350  logf1o  24356  dvlog  24442  asinrebnd  24673  sqff1o  24953  lgsqrlem4  25119  cnvmot  25481  f1otrg  25796  f1otrge  25797  cnvunop  28905  unopadj  28906  fresf1o  29561  fmptco1f1o  29562  padct  29625  fcobij  29628  fsumiunle  29703  abliso  29824  madjusmdetlem2  30022  madjusmdetlem4  30024  tpr2rico  30086  esumiun  30284  reprpmtf1o  30832  derangenlem  31279  subfacp1lem4  31291  cvmfolem  31387  cvmliftlem6  31398  fv1stcnv  31804  fv2ndcnv  31805  f1ocan1fv  33651  f1ocan2fv  33652  ismtycnv  33731  ismtyima  33732  ismtyhmeolem  33733  ismtybndlem  33735  rngoisocnv  33910  lautcnv  35694  cdlemk45  36552  cdlemn9  36811  eldioph2  37642  kelac1  37950  brco2f1o  38647  brco3f1o  38648  sge0f1o  40917  mgmhmf1o  42112
  Copyright terms: Public domain W3C validator