Theorem f1ocnv 6846

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 6652	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6189	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6641	. . . . . 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 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6842	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6842	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 292	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ^◡ccnv 5676  Rel wrel 5682   Fn wfn 6539  –1-1-onto→wf1o 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551

This theorem is referenced by:  f1ocnvb  6847  f1orescnv  6849  f1imacnv  6850  f1cnv  6858  f1ococnv1  6863  f1oresrab  7125  f1ocnvfv2  7275  f1ocnvdm  7283  f1ocnvfvrneq  7284  fcof1oinvd  7291  fveqf1o  7301  isocnv  7327  weniso  7351  f1ofveu  7403  f1oexrnex  7918  f1oexbi  7919  fnwelem  8117  oacomf1o  8565  mapsnf1o3  8889  ener  8997  en0  9013  en0OLD  9014  en0ALT  9015  en1  9021  en1OLD  9022  omf1o  9075  domss2  9136  mapen  9141  ssenen  9151  f1oenfirn  9183  ensymfib  9187  snnen2o  9237  1sdom2dom  9247  infn0  9307  f1fi  9339  f1opwfi  9356  mapfienlem2  9401  mapfienlem3  9402  mapfien  9403  mapfien2  9404  ordiso2  9510  unxpwdom2  9583  cantnfle  9666  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1d  9683  cantnflem1  9684  wemapwe  9692  oef1o  9693  cnfcomlem  9694  cnfcom  9695  cnfcom2lem  9696  cnfcom2  9697  cnfcom3lem  9698  cnfcom3  9699  infxpenlem  10008  infxpenc  10013  dfac8b  10026  acndom  10046  acndom2  10049  iunfictbso  10109  dfac12lem2  10139  infpssrlem3  10300  infpssrlem4  10301  fin1a2lem7  10401  axcc3  10433  ttukeylem7  10510  fpwwe2lem5  10630  fpwwe2lem6  10631  pwfseqlem5  10658  axdc4uzlem  13948  seqf1olem1  14007  seqf1olem2  14008  hashfacen  14413  hashfacenOLD  14414  seqcoll  14425  seqcoll2  14426  cnrecnv  15112  isercolllem2  15612  isercoll  15614  summolem3  15660  summolem2a  15661  ackbijnn  15774  prodmolem3  15877  prodmolem2a  15878  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  phimullem  16712  eulerthlem2  16715  unbenlem  16841  1arith2  16861  xpsbas  17518  xpsadd  17520  xpsmul  17521  xpssca  17522  xpsvsca  17523  xpsless  17524  xpsle  17525  setcinv  18040  catcisolem  18060  xpsmnd  18665  mhmf1o  18682  xpsgrp  18942  ghmf1o  19122  symggrp  19268  symginv  19270  f1omvdcnv  19312  f1omvdconj  19314  pmtrfconj  19334  odngen  19445  gsumval3eu  19772  gsumval3  19775  gsumzf1o  19780  xpsringd  20145  lmhmf1o  20657  fidomndrnglem  20925  znleval  21110  zntoslem  21112  znunithash  21120  psrass1lemOLD  21493  psrass1lem  21496  coe1sfi  21737  mdetleib2  22090  basqtop  23215  tgqtop  23216  reghmph  23297  indishmph  23302  cmphaushmeo  23304  ordthmeolem  23305  txhmeo  23307  xpstps  23314  xpstopnlem2  23315  qtopf1  23320  ufldom  23466  symgtgp  23610  tgpconncompeqg  23616  xpsdsfn  23883  xpsxmet  23886  xpsdsval  23887  xpsmet  23888  imasf1obl  23997  xpsxms  24043  xpsms  24044  iccpnfcnv  24460  xrhmeo  24462  ovoliunlem2  25020  vitalilem2  25126  mbfimaopnlem  25172  dvcnvlem  25493  dvcnv  25494  dvcnvrelem2  25535  dvcnvre  25536  efif1olem4  26054  eff1olem  26057  logrn  26067  logf1o  26073  dvlog  26159  asinrebnd  26406  sqff1o  26686  lgsqrlem4  26852  cnvmot  27823  f1otrg  28153  f1otrge  28154  cnvunop  31202  unopadj  31203  fresf1o  31886  fmptco1f1o  31888  padct  31975  fcobij  31978  fsumiunle  32066  abliso  32228  symgcom  32275  tocycfvres1  32300  tocycfvres2  32301  cycpmcl  32306  cycpmconjvlem  32331  cycpmconjv  32332  cycpmconjslem1  32344  cycpmconjslem2  32345  cycpmconjs  32346  madjusmdetlem2  32839  madjusmdetlem4  32841  tpr2rico  32923  esumiun  33123  reprpmtf1o  33669  derangenlem  34193  subfacp1lem4  34205  cvmfolem  34301  cvmliftlem6  34312  fv1stcnv  34779  fv2ndcnv  34780  f1ocan1fv  36642  f1ocan2fv  36643  ismtycnv  36718  ismtyima  36719  ismtyhmeolem  36720  ismtybndlem  36722  rngoisocnv  36897  lautcnv  39009  cdlemk45  39866  cdlemn9  40124  sticksstones18  41028  sticksstones19  41029  metakunt34  41066  eldioph2  41548  kelac1  41853  brco2f1o  42831  brco3f1o  42832  sge0f1o  45146  isomushgr  46542  isomgrsym  46552  mgmhmf1o  46605  xpsrngd  46728