Theorem f1ocnv 6794

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 6602	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6150	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6591	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 248	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 217	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 616	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6790	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6790	. 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 5630  Rel wrel 5636   Fn wfn 6494  –1-1-onto→wf1o 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1ocnvb  6795  f1orescnv  6797  f1imacnv  6798  f1cnv  6806  f1ococnv1  6811  f1oresrab  7081  f1ocnvfv2  7234  f1ocnvdm  7242  f1ocnvfvrneq  7243  fcof1oinvd  7250  fveqf1o  7259  isocnv  7287  weniso  7311  f1ofveu  7363  f1oexrnex  7883  f1oexbi  7884  fnwelem  8087  oacomf1o  8506  mapsnf1o3  8845  ener  8949  en0  8966  en0ALT  8967  en1  8972  omf1o  9021  domss2  9077  mapen  9082  ssenen  9092  f1oenfirn  9121  ensymfib  9125  snnen2o  9161  1sdom2dom  9170  infn0  9227  f1fi  9239  f1opwfi  9283  mapfienlem2  9333  mapfienlem3  9334  mapfien  9335  mapfien2  9336  ordiso2  9444  unxpwdom2  9517  cantnfle  9600  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1d  9617  cantnflem1  9618  wemapwe  9626  oef1o  9627  cnfcomlem  9628  cnfcom  9629  cnfcom2lem  9630  cnfcom2  9631  cnfcom3lem  9632  cnfcom3  9633  infxpenlem  9942  infxpenc  9947  dfac8b  9960  acndom  9980  acndom2  9983  iunfictbso  10043  dfac12lem2  10074  infpssrlem3  10234  infpssrlem4  10235  fin1a2lem7  10335  axcc3  10367  ttukeylem7  10444  fpwwe2lem5  10564  fpwwe2lem6  10565  pwfseqlem5  10592  axdc4uzlem  13924  seqf1olem1  13982  seqf1olem2  13983  hashfacen  14395  seqcoll  14405  seqcoll2  14406  cnrecnv  15107  isercolllem2  15608  isercoll  15610  summolem3  15656  summolem2a  15657  ackbijnn  15770  prodmolem3  15875  prodmolem2a  15876  sadcaddlem  16403  sadadd2lem  16405  sadadd3  16407  sadaddlem  16412  sadasslem  16416  sadeq  16418  phimullem  16725  eulerthlem2  16728  unbenlem  16855  1arith2  16875  xpsbas  17511  xpsadd  17513  xpsmul  17514  xpssca  17515  xpsvsca  17516  xpsless  17517  xpsle  17518  setcinv  18032  catcisolem  18052  mgmhmf1o  18609  xpsmnd  18686  mhmf1o  18705  xpsgrp  18973  ghmf1o  19162  symggrp  19314  symginv  19316  f1omvdcnv  19358  f1omvdconj  19360  pmtrfconj  19380  odngen  19491  gsumval3eu  19818  gsumval3  19821  gsumzf1o  19826  xpsrngd  20099  xpsringd  20252  fidomndrnglem  20692  lmhmf1o  20985  znleval  21496  zntoslem  21498  znunithash  21506  psrass1lem  21874  coe1sfi  22131  mdetleib2  22508  basqtop  23631  tgqtop  23632  reghmph  23713  indishmph  23718  cmphaushmeo  23720  ordthmeolem  23721  txhmeo  23723  xpstps  23730  xpstopnlem2  23731  qtopf1  23736  ufldom  23882  symgtgp  24026  tgpconncompeqg  24032  xpsdsfn  24298  xpsxmet  24301  xpsdsval  24302  xpsmet  24303  imasf1obl  24409  xpsxms  24455  xpsms  24456  iccpnfcnv  24875  xrhmeo  24877  ovoliunlem2  25437  vitalilem2  25543  mbfimaopnlem  25589  dvcnvlem  25913  dvcnv  25914  dvcnvrelem2  25956  dvcnvre  25957  efif1olem4  26487  eff1olem  26490  logrn  26500  logf1o  26506  dvlog  26593  asinrebnd  26844  sqff1o  27125  lgsqrlem4  27293  cnvmot  28521  f1otrg  28851  f1otrge  28852  cnvunop  31897  unopadj  31898  fresf1o  32605  fmptco1f1o  32607  padct  32693  fcobij  32695  fsumiunle  32804  ccatws1f1o  32923  mndlactf1o  33014  mndractf1o  33015  abliso  33020  gsumwrd2dccat  33050  symgcom  33055  tocycfvres1  33082  tocycfvres2  33083  cycpmcl  33088  cycpmconjvlem  33113  cycpmconjv  33114  cycpmconjslem1  33126  cycpmconjslem2  33127  cycpmconjs  33128  1arithidomlem2  33500  1arithidom  33501  madjusmdetlem2  33811  madjusmdetlem4  33813  tpr2rico  33895  esumiun  34077  reprpmtf1o  34610  derangenlem  35151  subfacp1lem4  35163  cvmfolem  35259  cvmliftlem6  35270  fv1stcnv  35757  fv2ndcnv  35758  f1ocan1fv  37713  f1ocan2fv  37714  ismtycnv  37789  ismtyima  37790  ismtyhmeolem  37791  ismtybndlem  37793  rngoisocnv  37968  lautcnv  40077  cdlemk45  40934  cdlemn9  41192  sticksstones18  42145  sticksstones19  42146  eldioph2  42743  kelac1  43045  brco2f1o  44014  brco3f1o  44015  sge0f1o  46373  3f1oss1  47069  3f1oss2  47070  grimcnv  47881  gricushgr  47910  isubgr3stgrlem7  47964  uspgrlimlem1  47980  uspgrlimlem2  47981  uspgrlimlem3  47982  grlicsym  47998