Theorem f1ocnv 6621

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 6448	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6040	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6438	. . . . . 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 6617	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6617	. 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 1533  ^◡ccnv 5548  Rel wrel 5554   Fn wfn 6344  –1-1-onto→wf1o 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356

This theorem is referenced by:  f1ocnvb  6622  f1orescnv  6624  f1imacnv  6625  f1cnv  6632  f1ococnv1  6637  f1oresrab  6883  f1ocnvfv2  7028  f1ocnvdm  7035  f1ocnvfvrneq  7036  fcof1oinvd  7043  fveqf1o  7052  isocnv  7077  weniso  7101  f1ofveu  7145  f1oexrnex  7626  f1oexbi  7627  fnwelem  7819  oacomf1o  8185  mapsnf1o3  8453  ener  8550  en0  8566  en1  8570  omf1o  8614  domss2  8670  mapen  8675  ssenen  8685  f1fi  8805  f1opwfi  8822  mapfienlem2  8863  mapfienlem3  8864  mapfien  8865  mapfien2  8866  ordiso2  8973  unxpwdom2  9046  cantnfle  9128  cantnfp1lem3  9137  cantnflem1b  9143  cantnflem1d  9145  cantnflem1  9146  wemapwe  9154  oef1o  9155  cnfcomlem  9156  cnfcom  9157  cnfcom2lem  9158  cnfcom2  9159  cnfcom3lem  9160  cnfcom3  9161  infxpenlem  9433  infxpenc  9438  dfac8b  9451  acndom  9471  acndom2  9474  iunfictbso  9534  dfac12lem2  9564  infpssrlem3  9721  infpssrlem4  9722  fin1a2lem7  9822  axcc3  9854  ttukeylem7  9931  fpwwe2lem6  10051  fpwwe2lem7  10052  pwfseqlem5  10079  axdc4uzlem  13345  seqf1olem1  13403  seqf1olem2  13404  hashfacen  13806  seqcoll  13816  seqcoll2  13817  cnrecnv  14518  isercolllem2  15016  isercoll  15018  summolem3  15065  summolem2a  15066  ackbijnn  15177  prodmolem3  15281  prodmolem2a  15282  sadcaddlem  15800  sadadd2lem  15802  sadadd3  15804  sadaddlem  15809  sadasslem  15813  sadeq  15815  phimullem  16110  eulerthlem2  16113  unbenlem  16238  1arith2  16258  xpsbas  16839  xpsadd  16841  xpsmul  16842  xpssca  16843  xpsvsca  16844  xpsless  16845  xpsle  16846  setcinv  17344  catcisolem  17360  xpsmnd  17945  mhmf1o  17960  xpsgrp  18212  ghmf1o  18382  symggrp  18522  symginv  18524  f1omvdcnv  18566  f1omvdconj  18568  pmtrfconj  18588  odngen  18696  gsumval3eu  19018  gsumval3  19021  gsumzf1o  19026  lmhmf1o  19812  fidomndrnglem  20073  psrass1lem  20151  coe1sfi  20375  znleval  20695  zntoslem  20697  znunithash  20705  mdetleib2  21191  basqtop  22313  tgqtop  22314  reghmph  22395  indishmph  22400  cmphaushmeo  22402  ordthmeolem  22403  txhmeo  22405  xpstps  22412  xpstopnlem2  22413  qtopf1  22418  ufldom  22564  symgtgp  22708  tgpconncompeqg  22714  xpsdsfn  22981  xpsxmet  22984  xpsdsval  22985  xpsmet  22986  imasf1obl  23092  xpsxms  23138  xpsms  23139  iccpnfcnv  23542  xrhmeo  23544  ovoliunlem2  24098  vitalilem2  24204  mbfimaopnlem  24250  dvcnvlem  24567  dvcnv  24568  dvcnvrelem2  24609  dvcnvre  24610  efif1olem4  25123  eff1olem  25126  logrn  25136  logf1o  25142  dvlog  25228  asinrebnd  25473  sqff1o  25753  lgsqrlem4  25919  cnvmot  26321  f1otrg  26651  f1otrge  26652  cnvunop  29689  unopadj  29690  fresf1o  30370  fmptco1f1o  30372  padct  30449  fcobij  30452  fsumiunle  30540  abliso  30678  symgcom  30722  tocycfvres1  30747  tocycfvres2  30748  cycpmcl  30753  cycpmconjvlem  30778  cycpmconjv  30779  cycpmconjslem1  30791  cycpmconjslem2  30792  cycpmconjs  30793  madjusmdetlem2  31088  madjusmdetlem4  31090  tpr2rico  31150  esumiun  31348  reprpmtf1o  31892  derangenlem  32413  subfacp1lem4  32425  cvmfolem  32521  cvmliftlem6  32532  fv1stcnv  33015  fv2ndcnv  33016  f1ocan1fv  34995  f1ocan2fv  34996  ismtycnv  35074  ismtyima  35075  ismtyhmeolem  35076  ismtybndlem  35078  rngoisocnv  35253  lautcnv  37220  cdlemk45  38077  cdlemn9  38335  eldioph2  39352  kelac1  39656  brco2f1o  40375  brco3f1o  40376  sge0f1o  42658  isomushgr  43985  isomgrsym  43995  mgmhmf1o  44048