Theorem f1ocnv 6787

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 6595	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6148	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6584	. . . . . 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 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6783	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6783	. 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 1542  ^◡ccnv 5624  Rel wrel 5630   Fn wfn 6488  –1-1-onto→wf1o 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500

This theorem is referenced by:  f1ocnvb  6788  f1orescnv  6790  f1imacnv  6791  f1cnv  6799  f1ococnv1  6804  f1oresrab  7075  f1ocnvfv2  7226  f1ocnvdm  7234  f1ocnvfvrneq  7235  fcof1oinvd  7242  fveqf1o  7251  isocnv  7279  weniso  7303  f1ofveu  7355  f1oexrnex  7872  f1oexbi  7873  fnwelem  8075  oacomf1o  8494  mapsnf1o3  8837  ener  8942  en0  8959  en0ALT  8960  en1  8965  omf1o  9012  domss2  9068  mapen  9073  ssenen  9083  f1oenfirn  9108  ensymfib  9112  snnen2o  9149  1sdom2dom  9158  infn0  9206  f1fi  9218  f1opwfi  9260  mapfienlem2  9313  mapfienlem3  9314  mapfien  9315  mapfien2  9316  ordiso2  9424  unxpwdom2  9497  cantnfle  9586  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1d  9603  cantnflem1  9604  wemapwe  9612  oef1o  9613  cnfcomlem  9614  cnfcom  9615  cnfcom2lem  9616  cnfcom2  9617  cnfcom3lem  9618  cnfcom3  9619  infxpenlem  9929  infxpenc  9934  dfac8b  9947  acndom  9967  acndom2  9970  iunfictbso  10030  dfac12lem2  10061  infpssrlem3  10221  infpssrlem4  10222  fin1a2lem7  10322  axcc3  10354  ttukeylem7  10431  fpwwe2lem5  10552  fpwwe2lem6  10553  pwfseqlem5  10580  axdc4uzlem  13939  seqf1olem1  13997  seqf1olem2  13998  hashfacen  14410  seqcoll  14420  seqcoll2  14421  cnrecnv  15121  isercolllem2  15622  isercoll  15624  summolem3  15670  summolem2a  15671  ackbijnn  15787  prodmolem3  15892  prodmolem2a  15893  sadcaddlem  16420  sadadd2lem  16422  sadadd3  16424  sadaddlem  16429  sadasslem  16433  sadeq  16435  phimullem  16743  eulerthlem2  16746  unbenlem  16873  1arith2  16893  xpsbas  17530  xpsadd  17532  xpsmul  17533  xpssca  17534  xpsvsca  17535  xpsless  17536  xpsle  17537  setcinv  18051  catcisolem  18071  mgmhmf1o  18662  xpsmnd  18739  mhmf1o  18758  xpsgrp  19029  ghmf1o  19217  symggrp  19369  symginv  19371  f1omvdcnv  19413  f1omvdconj  19415  pmtrfconj  19435  odngen  19546  gsumval3eu  19873  gsumval3  19876  gsumzf1o  19881  xpsrngd  20154  xpsringd  20306  fidomndrnglem  20743  lmhmf1o  21036  znleval  21547  zntoslem  21549  znunithash  21557  psrass1lem  21925  coe1sfi  22190  mdetleib2  22566  basqtop  23689  tgqtop  23690  reghmph  23771  indishmph  23776  cmphaushmeo  23778  ordthmeolem  23779  txhmeo  23781  xpstps  23788  xpstopnlem2  23789  qtopf1  23794  ufldom  23940  symgtgp  24084  tgpconncompeqg  24090  xpsdsfn  24355  xpsxmet  24358  xpsdsval  24359  xpsmet  24360  imasf1obl  24466  xpsxms  24512  xpsms  24513  iccpnfcnv  24924  xrhmeo  24926  ovoliunlem2  25483  vitalilem2  25589  mbfimaopnlem  25635  dvcnvlem  25956  dvcnv  25957  dvcnvrelem2  25998  dvcnvre  25999  efif1olem4  26525  eff1olem  26528  logrn  26538  logf1o  26544  dvlog  26631  asinrebnd  26881  sqff1o  27162  lgsqrlem4  27329  oldfib  28386  cnvmot  28626  f1otrg  28956  f1otrge  28957  cnvunop  32007  unopadj  32008  fresf1o  32722  fmptco1f1o  32724  padct  32809  fcobij  32811  fsumiunle  32920  ccatws1f1o  33029  mndlactf1o  33108  mndractf1o  33109  abliso  33114  gsumwrd2dccat  33157  symgcom  33162  tocycfvres1  33189  tocycfvres2  33190  cycpmcl  33195  cycpmconjvlem  33220  cycpmconjv  33221  cycpmconjslem1  33233  cycpmconjslem2  33234  cycpmconjs  33235  1arithidomlem2  33614  1arithidom  33615  mplvrpmrhm  33709  esplysply  33733  madjusmdetlem2  33991  madjusmdetlem4  33993  tpr2rico  34075  esumiun  34257  reprpmtf1o  34789  derangenlem  35372  subfacp1lem4  35384  cvmfolem  35480  cvmliftlem6  35491  fv1stcnv  35978  fv2ndcnv  35979  f1ocan1fv  38064  f1ocan2fv  38065  ismtycnv  38140  ismtyima  38141  ismtyhmeolem  38142  ismtybndlem  38144  rngoisocnv  38319  lautcnv  40553  cdlemk45  41410  cdlemn9  41668  sticksstones18  42620  sticksstones19  42621  eldioph2  43211  kelac1  43512  brco2f1o  44480  brco3f1o  44481  sge0f1o  46831  3f1oss1  47538  3f1oss2  47539  grimcnv  48379  gricushgr  48408  isubgr3stgrlem7  48463  uspgrlimlem1  48479  uspgrlimlem2  48480  uspgrlimlem3  48481  grlicsym  48504