Theorem f1ocnv 6859

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 6669	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6208	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6658	. . . . . 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 6855	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6855	. 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 1539  ^◡ccnv 5683  Rel wrel 5689   Fn wfn 6555  –1-1-onto→wf1o 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567

This theorem is referenced by:  f1ocnvb  6860  f1orescnv  6862  f1imacnv  6863  f1cnv  6871  f1ococnv1  6876  f1oresrab  7146  f1ocnvfv2  7298  f1ocnvdm  7306  f1ocnvfvrneq  7307  fcof1oinvd  7314  fveqf1o  7323  isocnv  7351  weniso  7375  f1ofveu  7426  f1oexrnex  7950  f1oexbi  7951  fnwelem  8157  oacomf1o  8604  mapsnf1o3  8936  ener  9042  en0  9059  en0ALT  9060  en1  9065  omf1o  9116  domss2  9177  mapen  9182  ssenen  9192  f1oenfirn  9221  ensymfib  9225  snnen2o  9274  1sdom2dom  9284  infn0  9341  f1fi  9353  f1opwfi  9397  mapfienlem2  9447  mapfienlem3  9448  mapfien  9449  mapfien2  9450  ordiso2  9556  unxpwdom2  9629  cantnfle  9712  cantnfp1lem3  9721  cantnflem1b  9727  cantnflem1d  9729  cantnflem1  9730  wemapwe  9738  oef1o  9739  cnfcomlem  9740  cnfcom  9741  cnfcom2lem  9742  cnfcom2  9743  cnfcom3lem  9744  cnfcom3  9745  infxpenlem  10054  infxpenc  10059  dfac8b  10072  acndom  10092  acndom2  10095  iunfictbso  10155  dfac12lem2  10186  infpssrlem3  10346  infpssrlem4  10347  fin1a2lem7  10447  axcc3  10479  ttukeylem7  10556  fpwwe2lem5  10676  fpwwe2lem6  10677  pwfseqlem5  10704  axdc4uzlem  14025  seqf1olem1  14083  seqf1olem2  14084  hashfacen  14494  seqcoll  14504  seqcoll2  14505  cnrecnv  15205  isercolllem2  15703  isercoll  15705  summolem3  15751  summolem2a  15752  ackbijnn  15865  prodmolem3  15970  prodmolem2a  15971  sadcaddlem  16495  sadadd2lem  16497  sadadd3  16499  sadaddlem  16504  sadasslem  16508  sadeq  16510  phimullem  16817  eulerthlem2  16820  unbenlem  16947  1arith2  16967  xpsbas  17618  xpsadd  17620  xpsmul  17621  xpssca  17622  xpsvsca  17623  xpsless  17624  xpsle  17625  setcinv  18136  catcisolem  18156  mgmhmf1o  18714  xpsmnd  18791  mhmf1o  18810  xpsgrp  19078  ghmf1o  19267  symggrp  19419  symginv  19421  f1omvdcnv  19463  f1omvdconj  19465  pmtrfconj  19485  odngen  19596  gsumval3eu  19923  gsumval3  19926  gsumzf1o  19931  xpsrngd  20177  xpsringd  20330  fidomndrnglem  20774  lmhmf1o  21046  znleval  21574  zntoslem  21576  znunithash  21584  psrass1lem  21953  coe1sfi  22216  mdetleib2  22595  basqtop  23720  tgqtop  23721  reghmph  23802  indishmph  23807  cmphaushmeo  23809  ordthmeolem  23810  txhmeo  23812  xpstps  23819  xpstopnlem2  23820  qtopf1  23825  ufldom  23971  symgtgp  24115  tgpconncompeqg  24121  xpsdsfn  24388  xpsxmet  24391  xpsdsval  24392  xpsmet  24393  imasf1obl  24502  xpsxms  24548  xpsms  24549  iccpnfcnv  24976  xrhmeo  24978  ovoliunlem2  25539  vitalilem2  25645  mbfimaopnlem  25691  dvcnvlem  26015  dvcnv  26016  dvcnvrelem2  26058  dvcnvre  26059  efif1olem4  26588  eff1olem  26591  logrn  26601  logf1o  26607  dvlog  26694  asinrebnd  26945  sqff1o  27226  lgsqrlem4  27394  cnvmot  28550  f1otrg  28880  f1otrge  28881  cnvunop  31938  unopadj  31939  fresf1o  32642  fmptco1f1o  32644  padct  32732  fcobij  32734  fsumiunle  32832  ccatws1f1o  32937  mndlactf1o  33036  mndractf1o  33037  abliso  33042  gsumwrd2dccat  33071  symgcom  33104  tocycfvres1  33131  tocycfvres2  33132  cycpmcl  33137  cycpmconjvlem  33162  cycpmconjv  33163  cycpmconjslem1  33175  cycpmconjslem2  33176  cycpmconjs  33177  1arithidomlem2  33565  1arithidom  33566  madjusmdetlem2  33828  madjusmdetlem4  33830  tpr2rico  33912  esumiun  34096  reprpmtf1o  34642  derangenlem  35177  subfacp1lem4  35189  cvmfolem  35285  cvmliftlem6  35296  fv1stcnv  35778  fv2ndcnv  35779  f1ocan1fv  37734  f1ocan2fv  37735  ismtycnv  37810  ismtyima  37811  ismtyhmeolem  37812  ismtybndlem  37814  rngoisocnv  37989  lautcnv  40093  cdlemk45  40950  cdlemn9  41208  sticksstones18  42166  sticksstones19  42167  metakunt34  42240  eldioph2  42778  kelac1  43080  brco2f1o  44050  brco3f1o  44051  sge0f1o  46402  3f1oss1  47092  3f1oss2  47093  grimcnv  47884  gricushgr  47891  isubgr3stgrlem7  47944  uspgrlimlem1  47960  uspgrlimlem2  47961  uspgrlimlem3  47962  grlicsym  47978