Theorem f1ocnv 6834

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 6638	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6188	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6627	. . . . . 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 6830	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6830	. 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 1567  ^◡ccnv 5661  Rel wrel 5667   Fn wfn 6532  –1-1-onto→wf1o 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544

This theorem is referenced by:  f1ocnvb  6835  f1orescnv  6837  f1imacnv  6838  f1cnv  6846  f1ococnv1  6851  f1oresrab  7124  f1ocnvfv2  7276  f1ocnvdm  7284  f1ocnvfvrneq  7285  fcof1oinvd  7292  fveqf1o  7301  isocnv  7329  weniso  7353  f1ofveu  7405  f1oexrnex  7924  f1oexbi  7925  fnwelem  8127  oacomf1o  8550  mapsnf1o3  8893  ener  8998  en0  9015  en0ALT  9016  en1  9021  omf1o  9068  domss2  9124  mapen  9129  ssenen  9139  f1oenfirn  9164  ensymfib  9168  snnen2o  9205  1sdom2dom  9214  infn0  9262  f1fi  9274  f1opwfi  9313  mapfienlem2  9366  mapfienlem3  9367  mapfien  9368  mapfien2  9369  ordiso2  9477  unxpwdom2  9550  cantnfle  9640  cantnfp1lem3  9649  cantnflem1b  9655  cantnflem1d  9657  cantnflem1  9658  wemapwe  9666  oef1o  9667  cnfcomlem  9668  cnfcom  9669  cnfcom2lem  9670  cnfcom2  9671  cnfcom3lem  9672  cnfcom3  9673  infxpenlem  9997  infxpenc  10002  dfac8b  10015  acndom  10035  acndom2  10038  iunfictbso  10098  dfac12lem2  10128  infpssrlem3  10289  infpssrlem4  10290  fin1a2lem7  10390  axcc3  10422  ttukeylem7  10499  fpwwe2lem5  10620  fpwwe2lem6  10621  pwfseqlem5  10648  axdc4uzlem  14019  seqf1olem1  14077  seqf1olem2  14078  hashfacen  14491  seqcoll  14501  seqcoll2  14502  cnrecnv  15216  isercolllem2  15717  isercoll  15719  summolem3  15765  summolem2a  15766  ackbijnn  15882  prodmolem3  15987  prodmolem2a  15988  sadcaddlem  16515  sadadd2lem  16517  sadadd3  16519  sadaddlem  16524  sadasslem  16528  sadeq  16530  phimullem  16838  eulerthlem2  16841  unbenlem  16968  1arith2  16988  xpsbas  17626  xpsadd  17628  xpsmul  17629  xpssca  17630  xpsvsca  17631  xpsless  17632  xpsle  17633  setcinv  18147  catcisolem  18167  mgmhmf1o  18758  xpsmnd  18835  mhmf1o  18854  xpsgrp  19125  ghmf1o  19318  symggrp  19470  symginv  19472  f1omvdcnv  19514  f1omvdconj  19516  pmtrfconj  19536  odngen  19647  gsumval3eu  19974  gsumval3  19977  gsumzf1o  19982  xpsrngd  20257  xpsringd  20414  fidomndrnglem  20854  lmhmf1o  21145  znleval  21673  zntoslem  21675  znunithash  21683  psrass1lem  22052  coe1sfi  22342  mdetleib2  22714  basqtop  23837  tgqtop  23838  reghmph  23919  indishmph  23924  cmphaushmeo  23926  ordthmeolem  23927  txhmeo  23929  xpstps  23936  xpstopnlem2  23937  qtopf1  23942  ufldom  24088  symgtgp  24232  tgpconncompeqg  24238  xpsdsfn  24503  xpsxmet  24506  xpsdsval  24507  xpsmet  24508  imasf1obl  24614  xpsxms  24660  xpsms  24661  iccpnfcnv  25072  xrhmeo  25074  ovoliunlem2  25631  vitalilem2  25737  mbfimaopnlem  25783  dvcnvlem  26104  dvcnv  26105  dvcnvrelem2  26146  dvcnvre  26147  efif1olem4  26676  eff1olem  26679  logrn  26689  logf1o  26695  dvlog  26782  asinrebnd  27032  sqff1o  27312  lgsqrlem4  27479  oldfib  28536  cnvmot  28776  f1otrg  29161  f1otrge  29162  cnvunop  32211  unopadj  32212  fresf1o  32917  fmptco1f1o  32919  padct  33004  fcobij  33006  fsumiunle  33114  ccatws1f1o  33212  mndlactf1o  33291  mndractf1o  33292  abliso  33296  gsumwrd2dccat  33339  symgcom  33344  tocycfvres1  33371  tocycfvres2  33372  cycpmcl  33377  cycpmconjvlem  33402  cycpmconjv  33403  cycpmconjslem1  33415  cycpmconjslem2  33416  cycpmconjs  33417  1arithidomlem2  33771  1arithidom  33772  mplvrpmrhm  33882  esplysply  33906  madjusmdetlem2  34163  madjusmdetlem4  34165  tpr2rico  34247  esumiun  34429  reprpmtf1o  34958  derangenlem  35562  subfacp1lem4  35574  cvmfolem  35670  cvmliftlem6  35681  fv1stcnv  36168  fv2ndcnv  36169  f1ocan1fv  38265  f1ocan2fv  38266  ismtycnv  38341  ismtyima  38342  ismtyhmeolem  38343  ismtybndlem  38345  rngoisocnv  38520  lautcnv  40754  cdlemk45  41611  cdlemn9  41869  sticksstones18  42821  sticksstones19  42822  eldioph2  43385  kelac1  43682  brco2f1o  44650  brco3f1o  44651  sge0f1o  46988  3f1oss1  47701  3f1oss2  47702  grimcnv  48542  gricushgr  48571  isubgr3stgrlem7  48626  uspgrlimlem1  48642  uspgrlimlem2  48643  uspgrlimlem3  48644  grlicsym  48667