Theorem f1ocnv 6837

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 6641	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6189	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6630	. . . . . 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 628	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6833	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6833	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 295	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ^◡ccnv 5662  Rel wrel 5668   Fn wfn 6535  –1-1-onto→wf1o 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547

This theorem is used by:  f1ocnvb  6838  f1orescnv  6840  f1imacnv  6841  f1cnv  6849  f1ococnv1  6854  f1oresrab  7127  f1ocnvfv2  7284  f1ocnvdm  7292  f1ocnvfvrneq  7293  fcof1oinvd  7300  fveqf1o  7309  isocnv  7337  weniso  7363  f1ofveu  7413  f1oexrnex  7930  f1oexbi  7931  fnwelem  8133  oacomf1o  8556  mapsnf1o3  8899  ener  9004  en0  9021  en0ALT  9022  en1  9027  omf1o  9075  domss2  9131  mapen  9136  ssenen  9146  f1oenfirn  9171  ensymfib  9175  snnen2o  9212  1sdom2dom  9221  infn0  9269  f1fi  9281  f1opwfi  9320  mapfienlem2  9373  mapfienlem3  9374  mapfien  9375  mapfien2  9376  ordiso2  9484  unxpwdom2  9557  cantnfle  9647  cantnfp1lem3  9656  cantnflem1b  9662  cantnflem1d  9664  cantnflem1  9665  wemapwe  9673  oef1o  9674  cnfcomlem  9675  cnfcom  9676  cnfcom2lem  9677  cnfcom2  9678  cnfcom3lem  9679  cnfcom3  9680  infxpenlem  10013  infxpenc  10018  dfac8b  10031  acndom  10051  acndom2  10054  iunfictbso  10114  dfac12lem2  10144  infpssrlem3  10304  infpssrlem4  10305  fin1a2lem7  10405  axcc3  10437  ttukeylem7  10514  fpwwe2lem5  10637  fpwwe2lem6  10638  pwfseqlem5  10665  axdc4uzlem  14039  seqf1olem1  14097  seqf1olem2  14098  hashfacen  14511  seqcoll  14521  seqcoll2  14522  cnrecnv  15242  isercolllem2  15743  isercoll  15745  summolem3  15790  summolem2a  15791  ackbijnn  15907  prodmolem3  16012  prodmolem2a  16013  sadcaddlem  16539  sadadd2lem  16541  sadadd3  16543  sadaddlem  16548  sadasslem  16552  sadeq  16554  phimullem  16862  eulerthlem2  16865  unbenlem  16992  1arith2  17012  xpsbas  17650  xpsadd  17652  xpsmul  17653  xpssca  17654  xpsvsca  17655  xpsless  17656  xpsle  17657  setcinv  18171  catcisolem  18191  mgmhmf1o  18792  xpsmnd  18874  mhmf1o  18893  xpsgrp  19171  ghmf1o  19364  symggrp  19516  symginv  19518  f1omvdcnv  19560  f1omvdconj  19562  pmtrfconj  19582  odngen  19693  gsumval3eu  20020  gsumval3  20023  gsumzf1o  20028  xpsrngd  20303  xpsringd  20462  fidomndrnglem  20928  lmhmf1o  21219  znleval  21756  zntoslem  21758  znunithash  21766  psrass1lem  22135  coe1sfi  22425  mdetleib2  22797  basqtop  23921  tgqtop  23922  reghmph  24003  indishmph  24008  cmphaushmeo  24010  ordthmeolem  24011  txhmeo  24013  xpstps  24020  xpstopnlem2  24021  qtopf1  24026  ufldom  24172  symgtgp  24316  tgpconncompeqg  24322  xpsdsfn  24587  xpsxmet  24590  xpsdsval  24591  xpsmet  24592  imasf1obl  24698  xpsxms  24744  xpsms  24745  iccpnfcnv  25156  xrhmeo  25158  ovoliunlem2  25715  vitalilem2  25821  mbfimaopnlem  25867  dvcnvlem  26188  dvcnv  26189  dvcnvrelem2  26230  dvcnvre  26231  efif1olem4  26763  eff1olem  26766  logrn  26776  logf1o  26782  dvlog  26869  asinrebnd  27119  sqff1o  27399  lgsqrlem4  27566  oldfib  28623  cnvmot  28863  f1otrg  29277  f1otrge  29278  cnvunop  32343  unopadj  32344  fresf1o  33049  fmptco1f1o  33051  padct  33135  fcobij  33137  fsumiunle  33245  ccatws1f1o  33339  mndlactf1o  33416  mndractf1o  33417  abliso  33421  gsumwrd2dccat  33464  symgcom  33469  tocycfvres1  33496  tocycfvres2  33497  cycpmcl  33502  cycpmconjvlem  33527  cycpmconjv  33528  cycpmconjslem1  33540  cycpmconjslem2  33541  cycpmconjs  33542  1arithidomlem2  33892  1arithidom  33893  mplvrpmrhm  34003  esplysply  34027  madjusmdetlem2  34284  madjusmdetlem4  34286  tpr2rico  34368  esumiun  34550  reprpmtf1o  35080  derangenlem  35702  subfacp1lem4  35714  cvmfolem  35810  cvmliftlem6  35821  fv1stcnv  36308  fv2ndcnv  36309  f1ocan1fv  38437  f1ocan2fv  38438  ismtycnv  38513  ismtyima  38514  ismtyhmeolem  38515  ismtybndlem  38517  rngoisocnv  38692  lautcnv  40924  cdlemk45  41781  cdlemn9  42039  sticksstones18  42991  sticksstones19  42992  eldioph2  43553  kelac1  43850  brco2f1o  44818  brco3f1o  44819  sge0f1o  47156  3f1oss1  47872  3f1oss2  47873  grimcnv  48713  gricushgr  48742  isubgr3stgrlem7  48797  uspgrlimlem1  48813  uspgrlimlem2  48814  uspgrlimlem3  48815  grlicsym  48838