Theorem f1ocnv 6779

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 6587	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6140	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6576	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 249	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 218	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 622	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6775	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6775	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 293	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ^◡ccnv 5617  Rel wrel 5623   Fn wfn 6480  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1ocnvb  6780  f1orescnv  6782  f1imacnv  6783  f1cnv  6791  f1ococnv1  6796  f1oresrab  7069  f1ocnvfv2  7221  f1ocnvdm  7229  f1ocnvfvrneq  7230  fcof1oinvd  7237  fveqf1o  7246  isocnv  7274  weniso  7298  f1ofveu  7350  f1oexrnex  7867  f1oexbi  7868  fnwelem  8071  oacomf1o  8490  mapsnf1o3  8833  ener  8938  en0  8955  en0ALT  8956  en1  8961  omf1o  9008  domss2  9064  mapen  9069  ssenen  9079  f1oenfirn  9104  ensymfib  9108  snnen2o  9145  1sdom2dom  9154  infn0  9202  f1fi  9214  f1opwfi  9256  mapfienlem2  9309  mapfienlem3  9310  mapfien  9311  mapfien2  9312  ordiso2  9420  unxpwdom2  9493  cantnfle  9583  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  wemapwe  9609  oef1o  9610  cnfcomlem  9611  cnfcom  9612  cnfcom2lem  9613  cnfcom2  9614  cnfcom3lem  9615  cnfcom3  9616  infxpenlem  9926  infxpenc  9931  dfac8b  9944  acndom  9964  acndom2  9967  iunfictbso  10027  dfac12lem2  10058  infpssrlem3  10218  infpssrlem4  10219  fin1a2lem7  10319  axcc3  10351  ttukeylem7  10428  fpwwe2lem5  10549  fpwwe2lem6  10550  pwfseqlem5  10577  axdc4uzlem  13936  seqf1olem1  13994  seqf1olem2  13995  hashfacen  14407  seqcoll  14417  seqcoll2  14418  cnrecnv  15118  isercolllem2  15619  isercoll  15621  summolem3  15667  summolem2a  15668  ackbijnn  15784  prodmolem3  15889  prodmolem2a  15890  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  phimullem  16740  eulerthlem2  16743  unbenlem  16870  1arith2  16890  xpsbas  17527  xpsadd  17529  xpsmul  17530  xpssca  17531  xpsvsca  17532  xpsless  17533  xpsle  17534  setcinv  18048  catcisolem  18068  mgmhmf1o  18659  xpsmnd  18736  mhmf1o  18755  xpsgrp  19026  ghmf1o  19214  symggrp  19366  symginv  19368  f1omvdcnv  19410  f1omvdconj  19412  pmtrfconj  19432  odngen  19543  gsumval3eu  19870  gsumval3  19873  gsumzf1o  19878  xpsrngd  20151  xpsringd  20303  fidomndrnglem  20744  lmhmf1o  21036  znleval  21529  zntoslem  21531  znunithash  21539  psrass1lem  21908  coe1sfi  22198  mdetleib2  22571  basqtop  23694  tgqtop  23695  reghmph  23776  indishmph  23781  cmphaushmeo  23783  ordthmeolem  23784  txhmeo  23786  xpstps  23793  xpstopnlem2  23794  qtopf1  23799  ufldom  23945  symgtgp  24089  tgpconncompeqg  24095  xpsdsfn  24360  xpsxmet  24363  xpsdsval  24364  xpsmet  24365  imasf1obl  24471  xpsxms  24517  xpsms  24518  iccpnfcnv  24929  xrhmeo  24931  ovoliunlem2  25488  vitalilem2  25594  mbfimaopnlem  25640  dvcnvlem  25961  dvcnv  25962  dvcnvrelem2  26003  dvcnvre  26004  efif1olem4  26527  eff1olem  26530  logrn  26540  logf1o  26546  dvlog  26633  asinrebnd  26883  sqff1o  27163  lgsqrlem4  27330  oldfib  28387  cnvmot  28627  f1otrg  28957  f1otrge  28958  cnvunop  32007  unopadj  32008  fresf1o  32723  fmptco1f1o  32725  padct  32810  fcobij  32812  fsumiunle  32921  ccatws1f1o  33030  mndlactf1o  33109  mndractf1o  33110  abliso  33115  gsumwrd2dccat  33159  symgcom  33164  tocycfvres1  33191  tocycfvres2  33192  cycpmcl  33197  cycpmconjvlem  33222  cycpmconjv  33223  cycpmconjslem1  33235  cycpmconjslem2  33236  cycpmconjs  33237  1arithidomlem2  33619  1arithidom  33620  mplvrpmrhm  33731  esplysply  33755  madjusmdetlem2  34012  madjusmdetlem4  34014  tpr2rico  34096  esumiun  34278  reprpmtf1o  34810  derangenlem  35399  subfacp1lem4  35411  cvmfolem  35507  cvmliftlem6  35518  fv1stcnv  36005  fv2ndcnv  36006  f1ocan1fv  38093  f1ocan2fv  38094  ismtycnv  38169  ismtyima  38170  ismtyhmeolem  38171  ismtybndlem  38173  rngoisocnv  38348  lautcnv  40582  cdlemk45  41439  cdlemn9  41697  sticksstones18  42649  sticksstones19  42650  eldioph2  43211  kelac1  43508  brco2f1o  44476  brco3f1o  44477  sge0f1o  46825  3f1oss1  47538  3f1oss2  47539  grimcnv  48379  gricushgr  48408  isubgr3stgrlem7  48463  uspgrlimlem1  48479  uspgrlimlem2  48480  uspgrlimlem3  48481  grlicsym  48504