Theorem f1ocnv 6845

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 6651	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6188	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6640	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 247	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 216	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 615	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6841	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6841	. 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 1540  ^◡ccnv 5675  Rel wrel 5681   Fn wfn 6538  –1-1-onto→wf1o 6542

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is referenced by:  f1ocnvb  6846  f1orescnv  6848  f1imacnv  6849  f1cnv  6857  f1ococnv1  6862  f1oresrab  7127  f1ocnvfv2  7278  f1ocnvdm  7286  f1ocnvfvrneq  7287  fcof1oinvd  7294  fveqf1o  7304  isocnv  7330  weniso  7354  f1ofveu  7406  f1oexrnex  7922  f1oexbi  7923  fnwelem  8122  oacomf1o  8571  mapsnf1o3  8895  ener  9003  en0  9019  en0OLD  9020  en0ALT  9021  en1  9027  en1OLD  9028  omf1o  9081  domss2  9142  mapen  9147  ssenen  9157  f1oenfirn  9189  ensymfib  9193  snnen2o  9243  1sdom2dom  9253  infn0  9313  f1fi  9345  f1opwfi  9362  mapfienlem2  9407  mapfienlem3  9408  mapfien  9409  mapfien2  9410  ordiso2  9516  unxpwdom2  9589  cantnfle  9672  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1d  9689  cantnflem1  9690  wemapwe  9698  oef1o  9699  cnfcomlem  9700  cnfcom  9701  cnfcom2lem  9702  cnfcom2  9703  cnfcom3lem  9704  cnfcom3  9705  infxpenlem  10014  infxpenc  10019  dfac8b  10032  acndom  10052  acndom2  10055  iunfictbso  10115  dfac12lem2  10145  infpssrlem3  10306  infpssrlem4  10307  fin1a2lem7  10407  axcc3  10439  ttukeylem7  10516  fpwwe2lem5  10636  fpwwe2lem6  10637  pwfseqlem5  10664  axdc4uzlem  13955  seqf1olem1  14014  seqf1olem2  14015  hashfacen  14420  hashfacenOLD  14421  seqcoll  14432  seqcoll2  14433  cnrecnv  15119  isercolllem2  15619  isercoll  15621  summolem3  15667  summolem2a  15668  ackbijnn  15781  prodmolem3  15884  prodmolem2a  15885  sadcaddlem  16405  sadadd2lem  16407  sadadd3  16409  sadaddlem  16414  sadasslem  16418  sadeq  16420  phimullem  16719  eulerthlem2  16722  unbenlem  16848  1arith2  16868  xpsbas  17525  xpsadd  17527  xpsmul  17528  xpssca  17529  xpsvsca  17530  xpsless  17531  xpsle  17532  setcinv  18050  catcisolem  18070  mgmhmf1o  18631  xpsmnd  18705  mhmf1o  18724  xpsgrp  18985  ghmf1o  19169  symggrp  19316  symginv  19318  f1omvdcnv  19360  f1omvdconj  19362  pmtrfconj  19382  odngen  19493  gsumval3eu  19820  gsumval3  19823  gsumzf1o  19828  xpsrngd  20080  xpsringd  20227  lmhmf1o  20890  fidomndrnglem  21214  znleval  21420  zntoslem  21422  znunithash  21430  psrass1lemOLD  21803  psrass1lem  21806  coe1sfi  22056  mdetleib2  22410  basqtop  23535  tgqtop  23536  reghmph  23617  indishmph  23622  cmphaushmeo  23624  ordthmeolem  23625  txhmeo  23627  xpstps  23634  xpstopnlem2  23635  qtopf1  23640  ufldom  23786  symgtgp  23930  tgpconncompeqg  23936  xpsdsfn  24203  xpsxmet  24206  xpsdsval  24207  xpsmet  24208  imasf1obl  24317  xpsxms  24363  xpsms  24364  iccpnfcnv  24789  xrhmeo  24791  ovoliunlem2  25352  vitalilem2  25458  mbfimaopnlem  25504  dvcnvlem  25828  dvcnv  25829  dvcnvrelem2  25871  dvcnvre  25872  efif1olem4  26394  eff1olem  26397  logrn  26407  logf1o  26413  dvlog  26499  asinrebnd  26747  sqff1o  27027  lgsqrlem4  27195  cnvmot  28225  f1otrg  28555  f1otrge  28556  cnvunop  31604  unopadj  31605  fresf1o  32288  fmptco1f1o  32290  padct  32377  fcobij  32380  fsumiunle  32468  abliso  32630  symgcom  32680  tocycfvres1  32705  tocycfvres2  32706  cycpmcl  32711  cycpmconjvlem  32736  cycpmconjv  32737  cycpmconjslem1  32749  cycpmconjslem2  32750  cycpmconjs  32751  madjusmdetlem2  33272  madjusmdetlem4  33274  tpr2rico  33356  esumiun  33556  reprpmtf1o  34102  derangenlem  34626  subfacp1lem4  34638  cvmfolem  34734  cvmliftlem6  34745  fv1stcnv  35218  fv2ndcnv  35219  f1ocan1fv  37058  f1ocan2fv  37059  ismtycnv  37134  ismtyima  37135  ismtyhmeolem  37136  ismtybndlem  37138  rngoisocnv  37313  lautcnv  39425  cdlemk45  40282  cdlemn9  40540  sticksstones18  41447  sticksstones19  41448  metakunt34  41485  eldioph2  41963  kelac1  42268  brco2f1o  43246  brco3f1o  43247  sge0f1o  45557  isomushgr  46953  isomgrsym  46963