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 6155	. . . . 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 617	. 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 1542  ^◡ccnv 5631  Rel wrel 5637   Fn wfn 6495  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1ocnvb  6795  f1orescnv  6797  f1imacnv  6798  f1cnv  6806  f1ococnv1  6811  f1oresrab  7082  f1ocnvfv2  7233  f1ocnvdm  7241  f1ocnvfvrneq  7242  fcof1oinvd  7249  fveqf1o  7258  isocnv  7286  weniso  7310  f1ofveu  7362  f1oexrnex  7879  f1oexbi  7880  fnwelem  8083  oacomf1o  8502  mapsnf1o3  8845  ener  8950  en0  8967  en0ALT  8968  en1  8973  omf1o  9020  domss2  9076  mapen  9081  ssenen  9091  f1oenfirn  9116  ensymfib  9120  snnen2o  9157  1sdom2dom  9166  infn0  9214  f1fi  9226  f1opwfi  9268  mapfienlem2  9321  mapfienlem3  9322  mapfien  9323  mapfien2  9324  ordiso2  9432  unxpwdom2  9505  cantnfle  9592  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  wemapwe  9618  oef1o  9619  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  infxpenlem  9935  infxpenc  9940  dfac8b  9953  acndom  9973  acndom2  9976  iunfictbso  10036  dfac12lem2  10067  infpssrlem3  10227  infpssrlem4  10228  fin1a2lem7  10328  axcc3  10360  ttukeylem7  10437  fpwwe2lem5  10558  fpwwe2lem6  10559  pwfseqlem5  10586  axdc4uzlem  13918  seqf1olem1  13976  seqf1olem2  13977  hashfacen  14389  seqcoll  14399  seqcoll2  14400  cnrecnv  15100  isercolllem2  15601  isercoll  15603  summolem3  15649  summolem2a  15650  ackbijnn  15763  prodmolem3  15868  prodmolem2a  15869  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  phimullem  16718  eulerthlem2  16721  unbenlem  16848  1arith2  16868  xpsbas  17505  xpsadd  17507  xpsmul  17508  xpssca  17509  xpsvsca  17510  xpsless  17511  xpsle  17512  setcinv  18026  catcisolem  18046  mgmhmf1o  18637  xpsmnd  18714  mhmf1o  18733  xpsgrp  19001  ghmf1o  19189  symggrp  19341  symginv  19343  f1omvdcnv  19385  f1omvdconj  19387  pmtrfconj  19407  odngen  19518  gsumval3eu  19845  gsumval3  19848  gsumzf1o  19853  xpsrngd  20126  xpsringd  20280  fidomndrnglem  20717  lmhmf1o  21010  znleval  21521  zntoslem  21523  znunithash  21531  psrass1lem  21900  coe1sfi  22166  mdetleib2  22544  basqtop  23667  tgqtop  23668  reghmph  23749  indishmph  23754  cmphaushmeo  23756  ordthmeolem  23757  txhmeo  23759  xpstps  23766  xpstopnlem2  23767  qtopf1  23772  ufldom  23918  symgtgp  24062  tgpconncompeqg  24068  xpsdsfn  24333  xpsxmet  24336  xpsdsval  24337  xpsmet  24338  imasf1obl  24444  xpsxms  24490  xpsms  24491  iccpnfcnv  24910  xrhmeo  24912  ovoliunlem2  25472  vitalilem2  25578  mbfimaopnlem  25624  dvcnvlem  25948  dvcnv  25949  dvcnvrelem2  25991  dvcnvre  25992  efif1olem4  26522  eff1olem  26525  logrn  26535  logf1o  26541  dvlog  26628  asinrebnd  26879  sqff1o  27160  lgsqrlem4  27328  oldfib  28385  cnvmot  28625  f1otrg  28955  f1otrge  28956  cnvunop  32006  unopadj  32007  fresf1o  32721  fmptco1f1o  32723  padct  32808  fcobij  32810  fsumiunle  32921  ccatws1f1o  33044  mndlactf1o  33123  mndractf1o  33124  abliso  33129  gsumwrd2dccat  33172  symgcom  33177  tocycfvres1  33204  tocycfvres2  33205  cycpmcl  33210  cycpmconjvlem  33235  cycpmconjv  33236  cycpmconjslem1  33248  cycpmconjslem2  33249  cycpmconjs  33250  1arithidomlem2  33629  1arithidom  33630  mplvrpmrhm  33724  esplysply  33748  madjusmdetlem2  34006  madjusmdetlem4  34008  tpr2rico  34090  esumiun  34272  reprpmtf1o  34804  derangenlem  35387  subfacp1lem4  35399  cvmfolem  35495  cvmliftlem6  35506  fv1stcnv  35993  fv2ndcnv  35994  f1ocan1fv  37977  f1ocan2fv  37978  ismtycnv  38053  ismtyima  38054  ismtyhmeolem  38055  ismtybndlem  38057  rngoisocnv  38232  lautcnv  40466  cdlemk45  41323  cdlemn9  41581  sticksstones18  42534  sticksstones19  42535  eldioph2  43119  kelac1  43420  brco2f1o  44388  brco3f1o  44389  sge0f1o  46740  3f1oss1  47435  3f1oss2  47436  grimcnv  48248  gricushgr  48277  isubgr3stgrlem7  48332  uspgrlimlem1  48348  uspgrlimlem2  48349  uspgrlimlem3  48350  grlicsym  48373