Theorem f1ocnv 6737

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 6544	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6097	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6533	. . . . . 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 616	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6733	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6733	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 292	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ^◡ccnv 5589  Rel wrel 5595   Fn wfn 6432  –1-1-onto→wf1o 6436

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444

This theorem is referenced by:  f1ocnvb  6738  f1orescnv  6740  f1imacnv  6741  f1cnv  6749  f1ococnv1  6754  f1oresrab  7008  f1ocnvfv2  7158  f1ocnvdm  7166  f1ocnvfvrneq  7167  fcof1oinvd  7174  fveqf1o  7184  isocnv  7210  weniso  7234  f1ofveu  7279  f1oexrnex  7783  f1oexbi  7784  fnwelem  7981  oacomf1o  8405  mapsnf1o3  8692  ener  8796  en0  8812  en0OLD  8813  en0ALT  8814  en1  8820  en1OLD  8821  omf1o  8871  domss2  8932  mapen  8937  ssenen  8947  f1oenfirn  8975  ensymfib  8979  snnen2o  9035  f1fi  9115  f1opwfi  9132  mapfienlem2  9174  mapfienlem3  9175  mapfien  9176  mapfien2  9177  ordiso2  9283  unxpwdom2  9356  cantnfle  9438  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1d  9455  cantnflem1  9456  wemapwe  9464  oef1o  9465  cnfcomlem  9466  cnfcom  9467  cnfcom2lem  9468  cnfcom2  9469  cnfcom3lem  9470  cnfcom3  9471  infxpenlem  9778  infxpenc  9783  dfac8b  9796  acndom  9816  acndom2  9819  iunfictbso  9879  dfac12lem2  9909  infpssrlem3  10070  infpssrlem4  10071  fin1a2lem7  10171  axcc3  10203  ttukeylem7  10280  fpwwe2lem5  10400  fpwwe2lem6  10401  pwfseqlem5  10428  axdc4uzlem  13712  seqf1olem1  13771  seqf1olem2  13772  hashfacen  14175  hashfacenOLD  14176  seqcoll  14187  seqcoll2  14188  cnrecnv  14885  isercolllem2  15386  isercoll  15388  summolem3  15435  summolem2a  15436  ackbijnn  15549  prodmolem3  15652  prodmolem2a  15653  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadaddlem  16182  sadasslem  16186  sadeq  16188  phimullem  16489  eulerthlem2  16492  unbenlem  16618  1arith2  16638  xpsbas  17292  xpsadd  17294  xpsmul  17295  xpssca  17296  xpsvsca  17297  xpsless  17298  xpsle  17299  setcinv  17814  catcisolem  17834  xpsmnd  18434  mhmf1o  18449  xpsgrp  18703  ghmf1o  18873  symggrp  19017  symginv  19019  f1omvdcnv  19061  f1omvdconj  19063  pmtrfconj  19083  odngen  19191  gsumval3eu  19514  gsumval3  19517  gsumzf1o  19522  lmhmf1o  20317  fidomndrnglem  20587  znleval  20771  zntoslem  20773  znunithash  20781  psrass1lemOLD  21152  psrass1lem  21155  coe1sfi  21393  mdetleib2  21746  basqtop  22871  tgqtop  22872  reghmph  22953  indishmph  22958  cmphaushmeo  22960  ordthmeolem  22961  txhmeo  22963  xpstps  22970  xpstopnlem2  22971  qtopf1  22976  ufldom  23122  symgtgp  23266  tgpconncompeqg  23272  xpsdsfn  23539  xpsxmet  23542  xpsdsval  23543  xpsmet  23544  imasf1obl  23653  xpsxms  23699  xpsms  23700  iccpnfcnv  24116  xrhmeo  24118  ovoliunlem2  24676  vitalilem2  24782  mbfimaopnlem  24828  dvcnvlem  25149  dvcnv  25150  dvcnvrelem2  25191  dvcnvre  25192  efif1olem4  25710  eff1olem  25713  logrn  25723  logf1o  25729  dvlog  25815  asinrebnd  26060  sqff1o  26340  lgsqrlem4  26506  cnvmot  26911  f1otrg  27241  f1otrge  27242  cnvunop  30289  unopadj  30290  fresf1o  30975  fmptco1f1o  30977  padct  31063  fcobij  31066  fsumiunle  31152  abliso  31314  symgcom  31361  tocycfvres1  31386  tocycfvres2  31387  cycpmcl  31392  cycpmconjvlem  31417  cycpmconjv  31418  cycpmconjslem1  31430  cycpmconjslem2  31431  cycpmconjs  31432  madjusmdetlem2  31787  madjusmdetlem4  31789  tpr2rico  31871  esumiun  32071  reprpmtf1o  32615  derangenlem  33142  subfacp1lem4  33154  cvmfolem  33250  cvmliftlem6  33261  fv1stcnv  33760  fv2ndcnv  33761  f1ocan1fv  35893  f1ocan2fv  35894  ismtycnv  35969  ismtyima  35970  ismtyhmeolem  35971  ismtybndlem  35973  rngoisocnv  36148  lautcnv  38111  cdlemk45  38968  cdlemn9  39226  sticksstones18  40127  sticksstones19  40128  metakunt34  40165  eldioph2  40591  kelac1  40895  brco2f1o  41649  brco3f1o  41650  sge0f1o  43927  isomushgr  45289  isomgrsym  45299  mgmhmf1o  45352