Theorem f1ocnv 6629

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 6456	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6048	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6446	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 250	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 219	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6625	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6625	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 294	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ^◡ccnv 5556  Rel wrel 5562   Fn wfn 6352  –1-1-onto→wf1o 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364

This theorem is referenced by:  f1ocnvb  6630  f1orescnv  6632  f1imacnv  6633  f1cnv  6640  f1ococnv1  6645  f1oresrab  6891  f1ocnvfv2  7036  f1ocnvdm  7043  f1ocnvfvrneq  7044  fcof1oinvd  7051  fveqf1o  7060  isocnv  7085  weniso  7109  f1ofveu  7153  f1oexrnex  7634  f1oexbi  7635  fnwelem  7827  oacomf1o  8193  mapsnf1o3  8461  ener  8558  en0  8574  en1  8578  omf1o  8622  domss2  8678  mapen  8683  ssenen  8693  f1fi  8813  f1opwfi  8830  mapfienlem2  8871  mapfienlem3  8872  mapfien  8873  mapfien2  8874  ordiso2  8981  unxpwdom2  9054  cantnfle  9136  cantnfp1lem3  9145  cantnflem1b  9151  cantnflem1d  9153  cantnflem1  9154  wemapwe  9162  oef1o  9163  cnfcomlem  9164  cnfcom  9165  cnfcom2lem  9166  cnfcom2  9167  cnfcom3lem  9168  cnfcom3  9169  infxpenlem  9441  infxpenc  9446  dfac8b  9459  acndom  9479  acndom2  9482  iunfictbso  9542  dfac12lem2  9572  infpssrlem3  9729  infpssrlem4  9730  fin1a2lem7  9830  axcc3  9862  ttukeylem7  9939  fpwwe2lem6  10059  fpwwe2lem7  10060  pwfseqlem5  10087  axdc4uzlem  13354  seqf1olem1  13412  seqf1olem2  13413  hashfacen  13815  seqcoll  13825  seqcoll2  13826  cnrecnv  14526  isercolllem2  15024  isercoll  15026  summolem3  15073  summolem2a  15074  ackbijnn  15185  prodmolem3  15289  prodmolem2a  15290  sadcaddlem  15808  sadadd2lem  15810  sadadd3  15812  sadaddlem  15817  sadasslem  15821  sadeq  15823  phimullem  16118  eulerthlem2  16121  unbenlem  16246  1arith2  16266  xpsbas  16847  xpsadd  16849  xpsmul  16850  xpssca  16851  xpsvsca  16852  xpsless  16853  xpsle  16854  setcinv  17352  catcisolem  17368  xpsmnd  17953  mhmf1o  17968  xpsgrp  18220  ghmf1o  18390  symggrp  18530  symginv  18532  f1omvdcnv  18574  f1omvdconj  18576  pmtrfconj  18596  odngen  18704  gsumval3eu  19026  gsumval3  19029  gsumzf1o  19034  lmhmf1o  19820  fidomndrnglem  20081  psrass1lem  20159  coe1sfi  20383  znleval  20703  zntoslem  20705  znunithash  20713  mdetleib2  21199  basqtop  22321  tgqtop  22322  reghmph  22403  indishmph  22408  cmphaushmeo  22410  ordthmeolem  22411  txhmeo  22413  xpstps  22420  xpstopnlem2  22421  qtopf1  22426  ufldom  22572  symgtgp  22716  tgpconncompeqg  22722  xpsdsfn  22989  xpsxmet  22992  xpsdsval  22993  xpsmet  22994  imasf1obl  23100  xpsxms  23146  xpsms  23147  iccpnfcnv  23550  xrhmeo  23552  ovoliunlem2  24106  vitalilem2  24212  mbfimaopnlem  24258  dvcnvlem  24575  dvcnv  24576  dvcnvrelem2  24617  dvcnvre  24618  efif1olem4  25131  eff1olem  25134  logrn  25144  logf1o  25150  dvlog  25236  asinrebnd  25481  sqff1o  25761  lgsqrlem4  25927  cnvmot  26329  f1otrg  26659  f1otrge  26660  cnvunop  29697  unopadj  29698  fresf1o  30378  fmptco1f1o  30380  padct  30457  fcobij  30460  fsumiunle  30547  abliso  30685  symgcom  30729  tocycfvres1  30754  tocycfvres2  30755  cycpmcl  30760  cycpmconjvlem  30785  cycpmconjv  30786  cycpmconjslem1  30798  cycpmconjslem2  30799  cycpmconjs  30800  madjusmdetlem2  31095  madjusmdetlem4  31097  tpr2rico  31157  esumiun  31355  reprpmtf1o  31899  derangenlem  32420  subfacp1lem4  32432  cvmfolem  32528  cvmliftlem6  32539  fv1stcnv  33022  fv2ndcnv  33023  f1ocan1fv  35003  f1ocan2fv  35004  ismtycnv  35082  ismtyima  35083  ismtyhmeolem  35084  ismtybndlem  35086  rngoisocnv  35261  lautcnv  37228  cdlemk45  38085  cdlemn9  38343  eldioph2  39366  kelac1  39670  brco2f1o  40389  brco3f1o  40390  sge0f1o  42671  isomushgr  43998  isomgrsym  44008  mgmhmf1o  44061