Theorem f1ocnv 6835

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 6645	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6183	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6634	. . . . . 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 6831	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6831	. 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 5658  Rel wrel 5664   Fn wfn 6531  –1-1-onto→wf1o 6535

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1ocnvb  6836  f1orescnv  6838  f1imacnv  6839  f1cnv  6847  f1ococnv1  6852  f1oresrab  7122  f1ocnvfv2  7275  f1ocnvdm  7283  f1ocnvfvrneq  7284  fcof1oinvd  7291  fveqf1o  7300  isocnv  7328  weniso  7352  f1ofveu  7404  f1oexrnex  7928  f1oexbi  7929  fnwelem  8135  oacomf1o  8582  mapsnf1o3  8914  ener  9020  en0  9037  en0ALT  9038  en1  9043  omf1o  9094  domss2  9155  mapen  9160  ssenen  9170  f1oenfirn  9199  ensymfib  9203  snnen2o  9250  1sdom2dom  9260  infn0  9317  f1fi  9329  f1opwfi  9373  mapfienlem2  9423  mapfienlem3  9424  mapfien  9425  mapfien2  9426  ordiso2  9534  unxpwdom2  9607  cantnfle  9690  cantnfp1lem3  9699  cantnflem1b  9705  cantnflem1d  9707  cantnflem1  9708  wemapwe  9716  oef1o  9717  cnfcomlem  9718  cnfcom  9719  cnfcom2lem  9720  cnfcom2  9721  cnfcom3lem  9722  cnfcom3  9723  infxpenlem  10032  infxpenc  10037  dfac8b  10050  acndom  10070  acndom2  10073  iunfictbso  10133  dfac12lem2  10164  infpssrlem3  10324  infpssrlem4  10325  fin1a2lem7  10425  axcc3  10457  ttukeylem7  10534  fpwwe2lem5  10654  fpwwe2lem6  10655  pwfseqlem5  10682  axdc4uzlem  14006  seqf1olem1  14064  seqf1olem2  14065  hashfacen  14477  seqcoll  14487  seqcoll2  14488  cnrecnv  15189  isercolllem2  15687  isercoll  15689  summolem3  15735  summolem2a  15736  ackbijnn  15849  prodmolem3  15954  prodmolem2a  15955  sadcaddlem  16481  sadadd2lem  16483  sadadd3  16485  sadaddlem  16490  sadasslem  16494  sadeq  16496  phimullem  16803  eulerthlem2  16806  unbenlem  16933  1arith2  16953  xpsbas  17591  xpsadd  17593  xpsmul  17594  xpssca  17595  xpsvsca  17596  xpsless  17597  xpsle  17598  setcinv  18108  catcisolem  18128  mgmhmf1o  18683  xpsmnd  18760  mhmf1o  18779  xpsgrp  19047  ghmf1o  19236  symggrp  19386  symginv  19388  f1omvdcnv  19430  f1omvdconj  19432  pmtrfconj  19452  odngen  19563  gsumval3eu  19890  gsumval3  19893  gsumzf1o  19898  xpsrngd  20144  xpsringd  20297  fidomndrnglem  20737  lmhmf1o  21009  znleval  21520  zntoslem  21522  znunithash  21530  psrass1lem  21897  coe1sfi  22154  mdetleib2  22531  basqtop  23654  tgqtop  23655  reghmph  23736  indishmph  23741  cmphaushmeo  23743  ordthmeolem  23744  txhmeo  23746  xpstps  23753  xpstopnlem2  23754  qtopf1  23759  ufldom  23905  symgtgp  24049  tgpconncompeqg  24055  xpsdsfn  24321  xpsxmet  24324  xpsdsval  24325  xpsmet  24326  imasf1obl  24432  xpsxms  24478  xpsms  24479  iccpnfcnv  24898  xrhmeo  24900  ovoliunlem2  25461  vitalilem2  25567  mbfimaopnlem  25613  dvcnvlem  25937  dvcnv  25938  dvcnvrelem2  25980  dvcnvre  25981  efif1olem4  26511  eff1olem  26514  logrn  26524  logf1o  26530  dvlog  26617  asinrebnd  26868  sqff1o  27149  lgsqrlem4  27317  cnvmot  28525  f1otrg  28855  f1otrge  28856  cnvunop  31904  unopadj  31905  fresf1o  32614  fmptco1f1o  32616  padct  32702  fcobij  32704  fsumiunle  32813  ccatws1f1o  32932  mndlactf1o  33030  mndractf1o  33031  abliso  33036  gsumwrd2dccat  33066  symgcom  33099  tocycfvres1  33126  tocycfvres2  33127  cycpmcl  33132  cycpmconjvlem  33157  cycpmconjv  33158  cycpmconjslem1  33170  cycpmconjslem2  33171  cycpmconjs  33172  1arithidomlem2  33556  1arithidom  33557  madjusmdetlem2  33864  madjusmdetlem4  33866  tpr2rico  33948  esumiun  34130  reprpmtf1o  34663  derangenlem  35198  subfacp1lem4  35210  cvmfolem  35306  cvmliftlem6  35317  fv1stcnv  35799  fv2ndcnv  35800  f1ocan1fv  37755  f1ocan2fv  37756  ismtycnv  37831  ismtyima  37832  ismtyhmeolem  37833  ismtybndlem  37835  rngoisocnv  38010  lautcnv  40114  cdlemk45  40971  cdlemn9  41229  sticksstones18  42182  sticksstones19  42183  eldioph2  42760  kelac1  43062  brco2f1o  44031  brco3f1o  44032  sge0f1o  46391  3f1oss1  47084  3f1oss2  47085  grimcnv  47881  gricushgr  47910  isubgr3stgrlem7  47964  uspgrlimlem1  47980  uspgrlimlem2  47981  uspgrlimlem3  47982  grlicsym  47998