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 6181	. . . . 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 5650  Rel wrel 5656   Fn wfn 6533  –1-1-onto→wf1o 6537

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545

This theorem is used by:  f1ocnvb  6838  f1orescnv  6840  f1imacnv  6841  f1cnv  6849  f1ococnv1  6854  f1oresrab  7128  f1ocnvfv2  7285  f1ocnvdm  7293  f1ocnvfvrneq  7294  fcof1oinvd  7301  fveqf1o  7310  isocnv  7338  weniso  7364  f1ofveu  7414  f1oexrnex  7939  f1oexbi  7940  fnwelem  8143  oacomf1o  8573  mapsnf1o3  8923  ener  9028  en0  9045  en0ALT  9046  en1  9051  omf1o  9099  domss2  9155  mapen  9160  ssenen  9170  f1oenfirn  9195  ensymfib  9199  snnen2o  9236  1sdom2dom  9245  infn0  9294  f1fi  9306  f1opwfi  9345  mapfienlem2  9398  mapfienlem3  9399  mapfien  9400  mapfien2  9401  ordiso2  9509  unxpwdom2  9582  cantnfle  9672  cantnfp1lem3  9681  cantnflem1b  9687  cantnflem1d  9689  cantnflem1  9690  wemapwe  9698  oef1o  9699  cnfcomlem  9700  cnfcom  9701  cnfcom2lem  9702  cnfcom2  9703  cnfcom3lem  9704  cnfcom3  9705  infxpenlem  10092  infxpenc  10097  dfac8b  10110  acndom  10130  acndom2  10133  iunfictbso  10193  dfac12lem2  10223  infpssrlem3  10383  infpssrlem4  10384  fin1a2lem7  10484  axcc3  10516  ttukeylem7  10593  fpwwe2lem5  10720  fpwwe2lem6  10721  pwfseqlem5  10748  axdc4uzlem  14126  seqf1olem1  14184  seqf1olem2  14185  hashfacen  14599  seqcoll  14609  seqcoll2  14610  cnrecnv  15332  isercolllem2  15833  isercoll  15835  summolem3  15880  summolem2a  15881  ackbijnn  15997  prodmolem3  16100  prodmolem2a  16101  sadcaddlem  16627  sadadd2lem  16629  sadadd3  16631  sadaddlem  16636  sadasslem  16640  sadeq  16642  phimullem  16956  eulerthlem2  16959  unbenlem  17086  1arith2  17106  xpsbas  17744  xpsadd  17746  xpsmul  17747  xpssca  17748  xpsvsca  17749  xpsless  17750  xpsle  17751  setcinv  18265  catcisolem  18285  mgmhmf1o  18889  xpsmnd  18971  mhmf1o  18991  xpsgrp  19269  ghmf1o  19462  symggrp  19614  symginv  19616  f1omvdcnv  19658  f1omvdconj  19660  pmtrfconj  19680  odngen  19791  gsumval3eu  20118  gsumval3  20121  gsumzf1o  20126  xpsrngd  20401  xpsringd  20562  fidomndrnglem  21030  lmhmf1o  21321  znleval  21860  zntoslem  21862  znunithash  21870  psrass1lem  22241  coe1sfi  22531  mdetleib2  22903  basqtop  24030  tgqtop  24031  reghmph  24112  indishmph  24117  cmphaushmeo  24119  ordthmeolem  24120  txhmeo  24122  xpstps  24129  xpstopnlem2  24130  qtopf1  24135  ufldom  24281  symgtgp  24425  tgpconncompeqg  24431  xpsdsfn  24696  xpsxmet  24699  xpsdsval  24700  xpsmet  24701  imasf1obl  24807  xpsxms  24853  xpsms  24854  iccpnfcnv  25265  xrhmeo  25267  ovoliunlem2  25824  vitalilem2  25930  mbfimaopnlem  25976  dvcnvlem  26296  dvcnv  26297  dvcnvrelem2  26338  dvcnvre  26339  efif1olem4  26873  eff1olem  26876  logrn  26886  logf1o  26892  dvlog  26979  asinrebnd  27229  sqff1o  27509  lgsqrlem4  27676  oldfib  28763  cnvmot  29004  f1otrg  29448  f1otrge  29449  cnvunop  32520  unopadj  32521  fresf1o  33225  fmptco1f1o  33227  padct  33310  fcobij  33312  fsumiunle  33420  ccatws1f1o  33514  mndlactf1o  33591  mndractf1o  33592  abliso  33596  gsumwrd2dccat  33639  symgcom  33644  tocycfvres1  33671  tocycfvres2  33672  cycpmcl  33677  cycpmconjvlem  33702  cycpmconjv  33703  cycpmconjslem1  33715  cycpmconjslem2  33716  cycpmconjs  33717  1arithidomlem2  34068  1arithidom  34069  mplvrpmrhm  34179  esplysply  34203  madjusmdetlem2  34460  madjusmdetlem4  34462  tpr2rico  34544  esumiun  34726  reprpmtf1o  35255  vonf1onprcf1ac  35894  derangenlem  35936  subfacp1lem4  35948  cvmfolem  36044  cvmliftlem6  36055  fv1stcnv  36541  fv2ndcnv  36542  f1ocan1fv  38660  f1ocan2fv  38661  ismtycnv  38736  ismtyima  38737  ismtyhmeolem  38738  ismtybndlem  38740  rngoisocnv  38915  lautcnv  41147  cdlemk45  42004  cdlemn9  42262  sticksstones18  43214  sticksstones19  43215  eldioph2  43772  kelac1  44064  brco2f1o  45031  brco3f1o  45032  sge0f1o  47391  3f1oss1  48144  3f1oss2  48145  grimcnv  48985  gricushgr  49014  isubgr3stgrlem7  49069  uspgrlimlem1  49085  uspgrlimlem2  49086  uspgrlimlem3  49087  grlicsym  49110