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  27792  f1otrg  28122  f1otrge  28123  cnvunop  31171  unopadj  31172  fresf1o  31855  fmptco1f1o  31857  padct  31944  fcobij  31947  fsumiunle  32035  abliso  32197  symgcom  32244  tocycfvres1  32269  tocycfvres2  32270  cycpmcl  32275  cycpmconjvlem  32300  cycpmconjv  32301  cycpmconjslem1  32313  cycpmconjslem2  32314  cycpmconjs  32315  madjusmdetlem2  32808  madjusmdetlem4  32810  tpr2rico  32892  esumiun  33092  reprpmtf1o  33638  derangenlem  34162  subfacp1lem4  34174  cvmfolem  34270  cvmliftlem6  34281  fv1stcnv  34748  fv2ndcnv  34749  f1ocan1fv  36594  f1ocan2fv  36595  ismtycnv  36670  ismtyima  36671  ismtyhmeolem  36672  ismtybndlem  36674  rngoisocnv  36849  lautcnv  38961  cdlemk45  39818  cdlemn9  40076  sticksstones18  40980  sticksstones19  40981  metakunt34  41018  eldioph2  41500  kelac1  41805  brco2f1o  42783  brco3f1o  42784  sge0f1o  45098  isomushgr  46494  isomgrsym  46504  mgmhmf1o  46557  xpsrngd  46680