Theorem f1ocnv 6775

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 6583	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6136	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6572	. . . . . 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 616	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6771	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6771	. 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 1541  ^◡ccnv 5613  Rel wrel 5619   Fn wfn 6476  –1-1-onto→wf1o 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1ocnvb  6776  f1orescnv  6778  f1imacnv  6779  f1cnv  6787  f1ococnv1  6792  f1oresrab  7060  f1ocnvfv2  7211  f1ocnvdm  7219  f1ocnvfvrneq  7220  fcof1oinvd  7227  fveqf1o  7236  isocnv  7264  weniso  7288  f1ofveu  7340  f1oexrnex  7857  f1oexbi  7858  fnwelem  8061  oacomf1o  8480  mapsnf1o3  8819  ener  8923  en0  8940  en0ALT  8941  en1  8946  omf1o  8993  domss2  9049  mapen  9054  ssenen  9064  f1oenfirn  9089  ensymfib  9093  snnen2o  9129  1sdom2dom  9138  infn0  9186  f1fi  9198  f1opwfi  9240  mapfienlem2  9290  mapfienlem3  9291  mapfien  9292  mapfien2  9293  ordiso2  9401  unxpwdom2  9474  cantnfle  9561  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1d  9578  cantnflem1  9579  wemapwe  9587  oef1o  9588  cnfcomlem  9589  cnfcom  9590  cnfcom2lem  9591  cnfcom2  9592  cnfcom3lem  9593  cnfcom3  9594  infxpenlem  9904  infxpenc  9909  dfac8b  9922  acndom  9942  acndom2  9945  iunfictbso  10005  dfac12lem2  10036  infpssrlem3  10196  infpssrlem4  10197  fin1a2lem7  10297  axcc3  10329  ttukeylem7  10406  fpwwe2lem5  10526  fpwwe2lem6  10527  pwfseqlem5  10554  axdc4uzlem  13890  seqf1olem1  13948  seqf1olem2  13949  hashfacen  14361  seqcoll  14371  seqcoll2  14372  cnrecnv  15072  isercolllem2  15573  isercoll  15575  summolem3  15621  summolem2a  15622  ackbijnn  15735  prodmolem3  15840  prodmolem2a  15841  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  sadeq  16383  phimullem  16690  eulerthlem2  16693  unbenlem  16820  1arith2  16840  xpsbas  17476  xpsadd  17478  xpsmul  17479  xpssca  17480  xpsvsca  17481  xpsless  17482  xpsle  17483  setcinv  17997  catcisolem  18017  mgmhmf1o  18608  xpsmnd  18685  mhmf1o  18704  xpsgrp  18972  ghmf1o  19160  symggrp  19312  symginv  19314  f1omvdcnv  19356  f1omvdconj  19358  pmtrfconj  19378  odngen  19489  gsumval3eu  19816  gsumval3  19819  gsumzf1o  19824  xpsrngd  20097  xpsringd  20250  fidomndrnglem  20687  lmhmf1o  20980  znleval  21491  zntoslem  21493  znunithash  21501  psrass1lem  21869  coe1sfi  22126  mdetleib2  22503  basqtop  23626  tgqtop  23627  reghmph  23708  indishmph  23713  cmphaushmeo  23715  ordthmeolem  23716  txhmeo  23718  xpstps  23725  xpstopnlem2  23726  qtopf1  23731  ufldom  23877  symgtgp  24021  tgpconncompeqg  24027  xpsdsfn  24292  xpsxmet  24295  xpsdsval  24296  xpsmet  24297  imasf1obl  24403  xpsxms  24449  xpsms  24450  iccpnfcnv  24869  xrhmeo  24871  ovoliunlem2  25431  vitalilem2  25537  mbfimaopnlem  25583  dvcnvlem  25907  dvcnv  25908  dvcnvrelem2  25950  dvcnvre  25951  efif1olem4  26481  eff1olem  26484  logrn  26494  logf1o  26500  dvlog  26587  asinrebnd  26838  sqff1o  27119  lgsqrlem4  27287  cnvmot  28519  f1otrg  28849  f1otrge  28850  cnvunop  31898  unopadj  31899  fresf1o  32613  fmptco1f1o  32615  padct  32701  fcobij  32703  fsumiunle  32812  ccatws1f1o  32932  mndlactf1o  33011  mndractf1o  33012  abliso  33017  gsumwrd2dccat  33047  symgcom  33052  tocycfvres1  33079  tocycfvres2  33080  cycpmcl  33085  cycpmconjvlem  33110  cycpmconjv  33111  cycpmconjslem1  33123  cycpmconjslem2  33124  cycpmconjs  33125  1arithidomlem2  33501  1arithidom  33502  mplvrpmrhm  33577  esplysply  33592  madjusmdetlem2  33841  madjusmdetlem4  33843  tpr2rico  33925  esumiun  34107  reprpmtf1o  34639  derangenlem  35215  subfacp1lem4  35227  cvmfolem  35323  cvmliftlem6  35334  fv1stcnv  35821  fv2ndcnv  35822  f1ocan1fv  37776  f1ocan2fv  37777  ismtycnv  37852  ismtyima  37853  ismtyhmeolem  37854  ismtybndlem  37856  rngoisocnv  38031  lautcnv  40199  cdlemk45  41056  cdlemn9  41314  sticksstones18  42267  sticksstones19  42268  eldioph2  42865  kelac1  43166  brco2f1o  44135  brco3f1o  44136  sge0f1o  46490  3f1oss1  47185  3f1oss2  47186  grimcnv  47998  gricushgr  48027  isubgr3stgrlem7  48082  uspgrlimlem1  48098  uspgrlimlem2  48099  uspgrlimlem3  48100  grlicsym  48123