Theorem f1ocnv 6784

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 6592	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6145	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6581	. . . . . 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 6780	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6780	. 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 5621  Rel wrel 5627   Fn wfn 6485  –1-1-onto→wf1o 6489

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 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497

This theorem is referenced by:  f1ocnvb  6785  f1orescnv  6787  f1imacnv  6788  f1cnv  6796  f1ococnv1  6801  f1oresrab  7070  f1ocnvfv2  7221  f1ocnvdm  7229  f1ocnvfvrneq  7230  fcof1oinvd  7237  fveqf1o  7246  isocnv  7274  weniso  7298  f1ofveu  7350  f1oexrnex  7867  f1oexbi  7868  fnwelem  8071  oacomf1o  8490  mapsnf1o3  8831  ener  8936  en0  8953  en0ALT  8954  en1  8959  omf1o  9006  domss2  9062  mapen  9067  ssenen  9077  f1oenfirn  9102  ensymfib  9106  snnen2o  9143  1sdom2dom  9152  infn0  9200  f1fi  9212  f1opwfi  9254  mapfienlem2  9307  mapfienlem3  9308  mapfien  9309  mapfien2  9310  ordiso2  9418  unxpwdom2  9491  cantnfle  9578  cantnfp1lem3  9587  cantnflem1b  9593  cantnflem1d  9595  cantnflem1  9596  wemapwe  9604  oef1o  9605  cnfcomlem  9606  cnfcom  9607  cnfcom2lem  9608  cnfcom2  9609  cnfcom3lem  9610  cnfcom3  9611  infxpenlem  9921  infxpenc  9926  dfac8b  9939  acndom  9959  acndom2  9962  iunfictbso  10022  dfac12lem2  10053  infpssrlem3  10213  infpssrlem4  10214  fin1a2lem7  10314  axcc3  10346  ttukeylem7  10423  fpwwe2lem5  10544  fpwwe2lem6  10545  pwfseqlem5  10572  axdc4uzlem  13904  seqf1olem1  13962  seqf1olem2  13963  hashfacen  14375  seqcoll  14385  seqcoll2  14386  cnrecnv  15086  isercolllem2  15587  isercoll  15589  summolem3  15635  summolem2a  15636  ackbijnn  15749  prodmolem3  15854  prodmolem2a  15855  sadcaddlem  16382  sadadd2lem  16384  sadadd3  16386  sadaddlem  16391  sadasslem  16395  sadeq  16397  phimullem  16704  eulerthlem2  16707  unbenlem  16834  1arith2  16854  xpsbas  17491  xpsadd  17493  xpsmul  17494  xpssca  17495  xpsvsca  17496  xpsless  17497  xpsle  17498  setcinv  18012  catcisolem  18032  mgmhmf1o  18623  xpsmnd  18700  mhmf1o  18719  xpsgrp  18987  ghmf1o  19175  symggrp  19327  symginv  19329  f1omvdcnv  19371  f1omvdconj  19373  pmtrfconj  19393  odngen  19504  gsumval3eu  19831  gsumval3  19834  gsumzf1o  19839  xpsrngd  20112  xpsringd  20266  fidomndrnglem  20703  lmhmf1o  20996  znleval  21507  zntoslem  21509  znunithash  21517  psrass1lem  21886  coe1sfi  22152  mdetleib2  22530  basqtop  23653  tgqtop  23654  reghmph  23735  indishmph  23740  cmphaushmeo  23742  ordthmeolem  23743  txhmeo  23745  xpstps  23752  xpstopnlem2  23753  qtopf1  23758  ufldom  23904  symgtgp  24048  tgpconncompeqg  24054  xpsdsfn  24319  xpsxmet  24322  xpsdsval  24323  xpsmet  24324  imasf1obl  24430  xpsxms  24476  xpsms  24477  iccpnfcnv  24896  xrhmeo  24898  ovoliunlem2  25458  vitalilem2  25564  mbfimaopnlem  25610  dvcnvlem  25934  dvcnv  25935  dvcnvrelem2  25977  dvcnvre  25978  efif1olem4  26508  eff1olem  26511  logrn  26521  logf1o  26527  dvlog  26614  asinrebnd  26865  sqff1o  27146  lgsqrlem4  27314  oldfib  28335  cnvmot  28562  f1otrg  28892  f1otrge  28893  cnvunop  31942  unopadj  31943  fresf1o  32658  fmptco1f1o  32660  padct  32746  fcobij  32748  fsumiunle  32859  ccatws1f1o  32982  mndlactf1o  33061  mndractf1o  33062  abliso  33067  gsumwrd2dccat  33109  symgcom  33114  tocycfvres1  33141  tocycfvres2  33142  cycpmcl  33147  cycpmconjvlem  33172  cycpmconjv  33173  cycpmconjslem1  33185  cycpmconjslem2  33186  cycpmconjs  33187  1arithidomlem2  33566  1arithidom  33567  mplvrpmrhm  33661  esplysply  33678  madjusmdetlem2  33934  madjusmdetlem4  33936  tpr2rico  34018  esumiun  34200  reprpmtf1o  34732  derangenlem  35314  subfacp1lem4  35326  cvmfolem  35422  cvmliftlem6  35433  fv1stcnv  35920  fv2ndcnv  35921  f1ocan1fv  37866  f1ocan2fv  37867  ismtycnv  37942  ismtyima  37943  ismtyhmeolem  37944  ismtybndlem  37946  rngoisocnv  38121  lautcnv  40289  cdlemk45  41146  cdlemn9  41404  sticksstones18  42357  sticksstones19  42358  eldioph2  42946  kelac1  43247  brco2f1o  44215  brco3f1o  44216  sge0f1o  46568  3f1oss1  47263  3f1oss2  47264  grimcnv  48076  gricushgr  48105  isubgr3stgrlem7  48160  uspgrlimlem1  48176  uspgrlimlem2  48177  uspgrlimlem3  48178  grlicsym  48201