Theorem f1ocnv 6833

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 6637	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6187	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6626	. . . . . 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 627	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6829	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6829	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 295	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ^◡ccnv 5660  Rel wrel 5666   Fn wfn 6531  –1-1-onto→wf1o 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1ocnvb  6834  f1orescnv  6836  f1imacnv  6837  f1cnv  6845  f1ococnv1  6850  f1oresrab  7123  f1ocnvfv2  7275  f1ocnvdm  7283  f1ocnvfvrneq  7284  fcof1oinvd  7291  fveqf1o  7300  isocnv  7328  weniso  7352  f1ofveu  7404  f1oexrnex  7920  f1oexbi  7921  fnwelem  8123  oacomf1o  8546  mapsnf1o3  8889  ener  8994  en0  9011  en0ALT  9012  en1  9017  omf1o  9064  domss2  9120  mapen  9125  ssenen  9135  f1oenfirn  9160  ensymfib  9164  snnen2o  9201  1sdom2dom  9210  infn0  9258  f1fi  9270  f1opwfi  9309  mapfienlem2  9362  mapfienlem3  9363  mapfien  9364  mapfien2  9365  ordiso2  9473  unxpwdom2  9546  cantnfle  9636  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1d  9653  cantnflem1  9654  wemapwe  9662  oef1o  9663  cnfcomlem  9664  cnfcom  9665  cnfcom2lem  9666  cnfcom2  9667  cnfcom3lem  9668  cnfcom3  9669  infxpenlem  9993  infxpenc  9998  dfac8b  10011  acndom  10031  acndom2  10034  iunfictbso  10094  dfac12lem2  10124  infpssrlem3  10284  infpssrlem4  10285  fin1a2lem7  10385  axcc3  10417  ttukeylem7  10494  fpwwe2lem5  10615  fpwwe2lem6  10616  pwfseqlem5  10643  axdc4uzlem  14015  seqf1olem1  14073  seqf1olem2  14074  hashfacen  14487  seqcoll  14497  seqcoll2  14498  cnrecnv  15212  isercolllem2  15713  isercoll  15715  summolem3  15761  summolem2a  15762  ackbijnn  15878  prodmolem3  15983  prodmolem2a  15984  sadcaddlem  16510  sadadd2lem  16512  sadadd3  16514  sadaddlem  16519  sadasslem  16523  sadeq  16525  phimullem  16833  eulerthlem2  16836  unbenlem  16963  1arith2  16983  xpsbas  17621  xpsadd  17623  xpsmul  17624  xpssca  17625  xpsvsca  17626  xpsless  17627  xpsle  17628  setcinv  18142  catcisolem  18162  mgmhmf1o  18753  xpsmnd  18830  mhmf1o  18849  xpsgrp  19120  ghmf1o  19313  symggrp  19465  symginv  19467  f1omvdcnv  19509  f1omvdconj  19511  pmtrfconj  19531  odngen  19642  gsumval3eu  19969  gsumval3  19972  gsumzf1o  19977  xpsrngd  20252  xpsringd  20410  fidomndrnglem  20876  lmhmf1o  21167  znleval  21704  zntoslem  21706  znunithash  21714  psrass1lem  22083  coe1sfi  22373  mdetleib2  22745  basqtop  23868  tgqtop  23869  reghmph  23950  indishmph  23955  cmphaushmeo  23957  ordthmeolem  23958  txhmeo  23960  xpstps  23967  xpstopnlem2  23968  qtopf1  23973  ufldom  24119  symgtgp  24263  tgpconncompeqg  24269  xpsdsfn  24534  xpsxmet  24537  xpsdsval  24538  xpsmet  24539  imasf1obl  24645  xpsxms  24691  xpsms  24692  iccpnfcnv  25103  xrhmeo  25105  ovoliunlem2  25662  vitalilem2  25768  mbfimaopnlem  25814  dvcnvlem  26135  dvcnv  26136  dvcnvrelem2  26177  dvcnvre  26178  efif1olem4  26710  eff1olem  26713  logrn  26723  logf1o  26729  dvlog  26816  asinrebnd  27066  sqff1o  27346  lgsqrlem4  27513  oldfib  28570  cnvmot  28810  f1otrg  29220  f1otrge  29221  cnvunop  32270  unopadj  32271  fresf1o  32976  fmptco1f1o  32978  padct  33063  fcobij  33065  fsumiunle  33173  ccatws1f1o  33271  mndlactf1o  33350  mndractf1o  33351  abliso  33355  gsumwrd2dccat  33398  symgcom  33403  tocycfvres1  33430  tocycfvres2  33431  cycpmcl  33436  cycpmconjvlem  33461  cycpmconjv  33462  cycpmconjslem1  33474  cycpmconjslem2  33475  cycpmconjs  33476  1arithidomlem2  33826  1arithidom  33827  mplvrpmrhm  33937  esplysply  33961  madjusmdetlem2  34218  madjusmdetlem4  34220  tpr2rico  34302  esumiun  34484  reprpmtf1o  35013  derangenlem  35663  subfacp1lem4  35675  cvmfolem  35771  cvmliftlem6  35782  fv1stcnv  36269  fv2ndcnv  36270  f1ocan1fv  38397  f1ocan2fv  38398  ismtycnv  38473  ismtyima  38474  ismtyhmeolem  38475  ismtybndlem  38477  rngoisocnv  38652  lautcnv  40884  cdlemk45  41741  cdlemn9  41999  sticksstones18  42951  sticksstones19  42952  eldioph2  43513  kelac1  43810  brco2f1o  44778  brco3f1o  44779  sge0f1o  47116  3f1oss1  47832  3f1oss2  47833  grimcnv  48673  gricushgr  48702  isubgr3stgrlem7  48757  uspgrlimlem1  48773  uspgrlimlem2  48774  uspgrlimlem3  48775  grlicsym  48798