Theorem f1ocnv 6602

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 6424	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6013	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6414	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 251	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 220	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 618	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6598	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6598	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 295	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  ^◡ccnv 5518  Rel wrel 5524   Fn wfn 6319  –1-1-onto→wf1o 6323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331

This theorem is referenced by:  f1ocnvb  6603  f1orescnv  6605  f1imacnv  6606  f1cnv  6613  f1ococnv1  6618  f1oresrab  6866  f1ocnvfv2  7012  f1ocnvdm  7019  f1ocnvfvrneq  7020  fcof1oinvd  7027  fveqf1o  7037  isocnv  7062  weniso  7086  f1ofveu  7130  f1oexrnex  7614  f1oexbi  7615  fnwelem  7808  oacomf1o  8174  mapsnf1o3  8442  ener  8539  en0  8555  en1  8559  omf1o  8603  domss2  8660  mapen  8665  ssenen  8675  f1fi  8795  f1opwfi  8812  mapfienlem2  8853  mapfienlem3  8854  mapfien  8855  mapfien2  8856  ordiso2  8963  unxpwdom2  9036  cantnfle  9118  cantnfp1lem3  9127  cantnflem1b  9133  cantnflem1d  9135  cantnflem1  9136  wemapwe  9144  oef1o  9145  cnfcomlem  9146  cnfcom  9147  cnfcom2lem  9148  cnfcom2  9149  cnfcom3lem  9150  cnfcom3  9151  infxpenlem  9424  infxpenc  9429  dfac8b  9442  acndom  9462  acndom2  9465  iunfictbso  9525  dfac12lem2  9555  infpssrlem3  9716  infpssrlem4  9717  fin1a2lem7  9817  axcc3  9849  ttukeylem7  9926  fpwwe2lem6  10046  fpwwe2lem7  10047  pwfseqlem5  10074  axdc4uzlem  13346  seqf1olem1  13405  seqf1olem2  13406  hashfacen  13808  seqcoll  13818  seqcoll2  13819  cnrecnv  14516  isercolllem2  15014  isercoll  15016  summolem3  15063  summolem2a  15064  ackbijnn  15175  prodmolem3  15279  prodmolem2a  15280  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  phimullem  16106  eulerthlem2  16109  unbenlem  16234  1arith2  16254  xpsbas  16837  xpsadd  16839  xpsmul  16840  xpssca  16841  xpsvsca  16842  xpsless  16843  xpsle  16844  setcinv  17342  catcisolem  17358  xpsmnd  17943  mhmf1o  17958  xpsgrp  18210  ghmf1o  18380  symggrp  18520  symginv  18522  f1omvdcnv  18564  f1omvdconj  18566  pmtrfconj  18586  odngen  18694  gsumval3eu  19017  gsumval3  19020  gsumzf1o  19025  lmhmf1o  19811  fidomndrnglem  20072  znleval  20246  zntoslem  20248  znunithash  20256  psrass1lem  20615  coe1sfi  20842  mdetleib2  21193  basqtop  22316  tgqtop  22317  reghmph  22398  indishmph  22403  cmphaushmeo  22405  ordthmeolem  22406  txhmeo  22408  xpstps  22415  xpstopnlem2  22416  qtopf1  22421  ufldom  22567  symgtgp  22711  tgpconncompeqg  22717  xpsdsfn  22984  xpsxmet  22987  xpsdsval  22988  xpsmet  22989  imasf1obl  23095  xpsxms  23141  xpsms  23142  iccpnfcnv  23549  xrhmeo  23551  ovoliunlem2  24107  vitalilem2  24213  mbfimaopnlem  24259  dvcnvlem  24579  dvcnv  24580  dvcnvrelem2  24621  dvcnvre  24622  efif1olem4  25137  eff1olem  25140  logrn  25150  logf1o  25156  dvlog  25242  asinrebnd  25487  sqff1o  25767  lgsqrlem4  25933  cnvmot  26335  f1otrg  26665  f1otrge  26666  cnvunop  29701  unopadj  29702  fresf1o  30390  fmptco1f1o  30392  padct  30481  fcobij  30484  fsumiunle  30571  abliso  30730  symgcom  30777  tocycfvres1  30802  tocycfvres2  30803  cycpmcl  30808  cycpmconjvlem  30833  cycpmconjv  30834  cycpmconjslem1  30846  cycpmconjslem2  30847  cycpmconjs  30848  madjusmdetlem2  31181  madjusmdetlem4  31183  tpr2rico  31265  esumiun  31463  reprpmtf1o  32007  derangenlem  32531  subfacp1lem4  32543  cvmfolem  32639  cvmliftlem6  32650  fv1stcnv  33133  fv2ndcnv  33134  f1ocan1fv  35164  f1ocan2fv  35165  ismtycnv  35240  ismtyima  35241  ismtyhmeolem  35242  ismtybndlem  35244  rngoisocnv  35419  lautcnv  37386  cdlemk45  38243  cdlemn9  38501  metakunt34  39383  eldioph2  39703  kelac1  40007  brco2f1o  40735  brco3f1o  40736  sge0f1o  43021  isomushgr  44344  isomgrsym  44354  mgmhmf1o  44407