Theorem f1ocnv 6867

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-1onto𝐵 → ◡𝐹:𝐵⟶1-1onto𝐴)

Proof of Theorem f1ocnv

Step	Hyp	Ref	Expression
1		fnrel 6671	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6199	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6660	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 251	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 220	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 39	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 628	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6863	. 2 ⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6863	. 2 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 295	1 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶1-1onto𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ^◡ccnv 5657  Rel wrel 5663   Fn wfn 6561  ⟶1-1ontowf1o 6565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573

This theorem is used by:  f1ocnvb  6868  f1orescnv  6870  f1imacnv  6871  f1cnv  6879  f1ococnv1  6885  f1oresrab  7160  f1ocnvfv2  7316  f1ocnvdm  7324  f1ocnvfvrneq  7325  fcof1oinvd  7332  fveqf1o  7341  isocnv  7369  weniso  7395  f1ofveu  7445  f1oexrnex  7973  f1oexbi  7974  fnwelem  8180  oacomf1o  8611  mapsnf1o3  8961  ener  9066  en0  9083  en0ALT  9084  en1  9089  omf1o  9137  domss2  9193  mapen  9198  ssenen  9208  f1oenfirn  9233  ensymfib  9237  snnen2o  9274  1sdom2dom  9283  infn0  9332  f1fi  9344  f1opwfi  9383  mapfienlem2  9435  mapfienlem3  9436  mapfien  9437  mapfien2  9438  ordiso2  9546  unxpwdom2  9619  cantnfle  9709  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1d  9726  cantnflem1  9727  wemapwe  9735  oef1o  9736  cnfcomlem  9737  cnfcom  9738  cnfcom2lem  9739  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  infxpenlem  10131  infxpenc  10136  dfac8b  10149  acndom  10169  acndom2  10172  iunfictbso  10232  dfac12lem2  10262  infpssrlem3  10422  infpssrlem4  10423  fin1a2lem7  10523  axcc3  10555  ttukeylem7  10632  fpwwe2lem5  10759  fpwwe2lem6  10760  pwfseqlem5  10787  axdc4uzlem  14166  seqf1olem1  14224  seqf1olem2  14225  hashfacen  14640  seqcoll  14650  seqcoll2  14651  cnrecnv  15375  isercolllem2  15877  isercoll  15879  summolem3  15924  summolem2a  15925  ackbijnn  16041  prodmolem3  16144  prodmolem2a  16145  sadcaddlem  16671  sadadd2lem  16673  sadadd3  16675  sadaddlem  16680  sadasslem  16684  sadeq  16686  phimullem  17000  eulerthlem2  17003  unbenlem  17130  1arith2  17150  xpsbas  17794  xpsadd  17796  xpsmul  17797  xpssca  17798  xpsvsca  17799  xpsless  17800  xpsle  17801  setcinv  18315  catcisolem  18335  mgmhmf1o  18939  xpsmnd  19021  mhmf1o  19041  xpsgrp  19319  ghmf1o  19512  symggrp  19665  symginv  19667  f1omvdcnv  19709  f1omvdconj  19711  pmtrfconj  19731  odngen  19842  gsumval3eu  20169  gsumval3  20172  gsumzf1o  20177  xpsrngd  20452  xpsringd  20613  fidomndrnglem  21081  lmhmf1o  21372  znleval  21915  zntoslem  21917  znunithash  21925  psrass1lem  22296  coe1sfi  22586  mdetleib2  22958  basqtop  24085  tgqtop  24086  reghmph  24167  indishmph  24172  cmphaushmeo  24174  ordthmeolem  24175  txhmeo  24177  xpstps  24184  xpstopnlem2  24185  qtopf1  24190  ufldom  24336  symgtgp  24480  tgpconncompeqg  24486  xpsdsfn  24751  xpsxmet  24754  xpsdsval  24755  xpsmet  24756  imasf1obl  24862  xpsxms  24908  xpsms  24909  iccpnfcnv  25320  xrhmeo  25322  ovoliunlem2  25879  vitalilem2  25985  mbfimaopnlem  26031  dvcnvlem  26351  dvcnv  26352  dvcnvrelem2  26393  dvcnvre  26394  efif1olem4  26930  eff1olem  26933  logrn  26943  logf1o  26949  dvlog  27036  asinrebnd  27286  sqff1o  27566  lgsqrlem4  27733  oldfib  28820  cnvmot  29061  f1otrg  29505  f1otrge  29506  cnvunop  32577  unopadj  32578  fresf1o  33323  fmptco1f1o  33325  padct  33407  fcobij  33408  fsumiunle  33516  ccatws1f1o  33610  mndlactf1o  33690  mndractf1o  33691  abliso  33695  gsumwrd2dccat  33738  symgcom  33743  tocycfvres1  33770  tocycfvres2  33771  cycpmcl  33776  cycpmconjvlem  33801  cycpmconjv  33802  cycpmconjslem1  33814  cycpmconjslem2  33815  cycpmconjs  33816  1arithidomlem2  34172  1arithidom  34173  mplvrpmrhm  34290  esplysply  34314  madjusmdetlem2  34571  madjusmdetlem4  34573  tpr2rico  34655  esumiun  34837  reprpmtf1o  35366  j0ltalephlem  36048  vonf1onprcf1ac  36085  prconf1acwevd  36089  onprcf1of1orad  36094  onprcf1of1orbd  36095  derangenlem  36144  subfacp1lem4  36156  cvmfolem  36252  cvmliftlem6  36263  fv1stcnv  36756  fv2ndcnv  36757  f1ocan1fv  38928  f1ocan2fv  38929  ismtycnv  39002  ismtyima  39003  ismtyhmeolem  39004  ismtybndlem  39006  rngoisocnv  39181  lautcnv  41413  cdlemk45  42270  cdlemn9  42528  sticksstones18  43480  sticksstones19  43481  eldioph2  44039  kelac1  44331  brco2f1o  45293  brco3f1o  45294  sge0f1o  47665  3f1oss1  48418  3f1oss2  48419  grimcnv  49259  gricushgr  49288  isubgr3stgrlem7  49343  uspgrlimlem1  49359  uspgrlimlem2  49360  uspgrlimlem3  49361  grlicsym  49384