Theorem f1ocnv 6874

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

Step	Hyp	Ref	Expression
1		fnrel 6681	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6220	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6670	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 248	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 217	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 615	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6870	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6870	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 292	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ^◡ccnv 5699  Rel wrel 5705   Fn wfn 6568  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  f1ocnvb  6875  f1orescnv  6877  f1imacnv  6878  f1cnv  6886  f1ococnv1  6891  f1oresrab  7161  f1ocnvfv2  7313  f1ocnvdm  7321  f1ocnvfvrneq  7322  fcof1oinvd  7329  fveqf1o  7338  isocnv  7366  weniso  7390  f1ofveu  7442  f1oexrnex  7967  f1oexbi  7968  fnwelem  8172  oacomf1o  8621  mapsnf1o3  8953  ener  9061  en0  9078  en0OLD  9079  en0ALT  9080  en1  9086  en1OLD  9087  omf1o  9141  domss2  9202  mapen  9207  ssenen  9217  f1oenfirn  9246  ensymfib  9250  snnen2o  9300  1sdom2dom  9310  infn0  9368  f1fi  9380  f1opwfi  9426  mapfienlem2  9475  mapfienlem3  9476  mapfien  9477  mapfien2  9478  ordiso2  9584  unxpwdom2  9657  cantnfle  9740  cantnfp1lem3  9749  cantnflem1b  9755  cantnflem1d  9757  cantnflem1  9758  wemapwe  9766  oef1o  9767  cnfcomlem  9768  cnfcom  9769  cnfcom2lem  9770  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  infxpenlem  10082  infxpenc  10087  dfac8b  10100  acndom  10120  acndom2  10123  iunfictbso  10183  dfac12lem2  10214  infpssrlem3  10374  infpssrlem4  10375  fin1a2lem7  10475  axcc3  10507  ttukeylem7  10584  fpwwe2lem5  10704  fpwwe2lem6  10705  pwfseqlem5  10732  axdc4uzlem  14034  seqf1olem1  14092  seqf1olem2  14093  hashfacen  14503  seqcoll  14513  seqcoll2  14514  cnrecnv  15214  isercolllem2  15714  isercoll  15716  summolem3  15762  summolem2a  15763  ackbijnn  15876  prodmolem3  15981  prodmolem2a  15982  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  sadaddlem  16512  sadasslem  16516  sadeq  16518  phimullem  16826  eulerthlem2  16829  unbenlem  16955  1arith2  16975  xpsbas  17632  xpsadd  17634  xpsmul  17635  xpssca  17636  xpsvsca  17637  xpsless  17638  xpsle  17639  setcinv  18157  catcisolem  18177  mgmhmf1o  18738  xpsmnd  18812  mhmf1o  18831  xpsgrp  19099  ghmf1o  19288  symggrp  19442  symginv  19444  f1omvdcnv  19486  f1omvdconj  19488  pmtrfconj  19508  odngen  19619  gsumval3eu  19946  gsumval3  19949  gsumzf1o  19954  xpsrngd  20206  xpsringd  20355  fidomndrnglem  20795  lmhmf1o  21068  znleval  21596  zntoslem  21598  znunithash  21606  psrass1lem  21975  coe1sfi  22236  mdetleib2  22615  basqtop  23740  tgqtop  23741  reghmph  23822  indishmph  23827  cmphaushmeo  23829  ordthmeolem  23830  txhmeo  23832  xpstps  23839  xpstopnlem2  23840  qtopf1  23845  ufldom  23991  symgtgp  24135  tgpconncompeqg  24141  xpsdsfn  24408  xpsxmet  24411  xpsdsval  24412  xpsmet  24413  imasf1obl  24522  xpsxms  24568  xpsms  24569  iccpnfcnv  24994  xrhmeo  24996  ovoliunlem2  25557  vitalilem2  25663  mbfimaopnlem  25709  dvcnvlem  26034  dvcnv  26035  dvcnvrelem2  26077  dvcnvre  26078  efif1olem4  26605  eff1olem  26608  logrn  26618  logf1o  26624  dvlog  26711  asinrebnd  26962  sqff1o  27243  lgsqrlem4  27411  cnvmot  28567  f1otrg  28897  f1otrge  28898  cnvunop  31950  unopadj  31951  fresf1o  32650  fmptco1f1o  32652  padct  32733  fcobij  32736  fsumiunle  32833  ccatws1f1o  32918  mndlactf1o  33016  mndractf1o  33017  abliso  33022  symgcom  33076  tocycfvres1  33103  tocycfvres2  33104  cycpmcl  33109  cycpmconjvlem  33134  cycpmconjv  33135  cycpmconjslem1  33147  cycpmconjslem2  33148  cycpmconjs  33149  1arithidomlem2  33529  1arithidom  33530  madjusmdetlem2  33774  madjusmdetlem4  33776  tpr2rico  33858  esumiun  34058  reprpmtf1o  34603  derangenlem  35139  subfacp1lem4  35151  cvmfolem  35247  cvmliftlem6  35258  fv1stcnv  35740  fv2ndcnv  35741  f1ocan1fv  37686  f1ocan2fv  37687  ismtycnv  37762  ismtyima  37763  ismtyhmeolem  37764  ismtybndlem  37766  rngoisocnv  37941  lautcnv  40047  cdlemk45  40904  cdlemn9  41162  sticksstones18  42121  sticksstones19  42122  metakunt34  42195  eldioph2  42718  kelac1  43020  brco2f1o  43994  brco3f1o  43995  sge0f1o  46303  3f1oss1  46990  3f1oss2  46991  grimcnv  47763  gricushgr  47770  uspgrlimlem1  47812  uspgrlimlem2  47813  uspgrlimlem3  47814  grlicsym  47830