Theorem f1ocnv 6776

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 6584	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6138	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6573	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 248	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 217	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 616	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6772	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6772	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 292	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ^◡ccnv 5618  Rel wrel 5624   Fn wfn 6477  –1-1-onto→wf1o 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  f1ocnvb  6777  f1orescnv  6779  f1imacnv  6780  f1cnv  6788  f1ococnv1  6793  f1oresrab  7061  f1ocnvfv2  7214  f1ocnvdm  7222  f1ocnvfvrneq  7223  fcof1oinvd  7230  fveqf1o  7239  isocnv  7267  weniso  7291  f1ofveu  7343  f1oexrnex  7860  f1oexbi  7861  fnwelem  8064  oacomf1o  8483  mapsnf1o3  8822  ener  8926  en0  8943  en0ALT  8944  en1  8949  omf1o  8997  domss2  9053  mapen  9058  ssenen  9068  f1oenfirn  9094  ensymfib  9098  snnen2o  9134  1sdom2dom  9143  infn0  9191  f1fi  9203  f1opwfi  9246  mapfienlem2  9296  mapfienlem3  9297  mapfien  9298  mapfien2  9299  ordiso2  9407  unxpwdom2  9480  cantnfle  9567  cantnfp1lem3  9576  cantnflem1b  9582  cantnflem1d  9584  cantnflem1  9585  wemapwe  9593  oef1o  9594  cnfcomlem  9595  cnfcom  9596  cnfcom2lem  9597  cnfcom2  9598  cnfcom3lem  9599  cnfcom3  9600  infxpenlem  9907  infxpenc  9912  dfac8b  9925  acndom  9945  acndom2  9948  iunfictbso  10008  dfac12lem2  10039  infpssrlem3  10199  infpssrlem4  10200  fin1a2lem7  10300  axcc3  10332  ttukeylem7  10409  fpwwe2lem5  10529  fpwwe2lem6  10530  pwfseqlem5  10557  axdc4uzlem  13890  seqf1olem1  13948  seqf1olem2  13949  hashfacen  14361  seqcoll  14371  seqcoll2  14372  cnrecnv  15072  isercolllem2  15573  isercoll  15575  summolem3  15621  summolem2a  15622  ackbijnn  15735  prodmolem3  15840  prodmolem2a  15841  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  sadeq  16383  phimullem  16690  eulerthlem2  16693  unbenlem  16820  1arith2  16840  xpsbas  17476  xpsadd  17478  xpsmul  17479  xpssca  17480  xpsvsca  17481  xpsless  17482  xpsle  17483  setcinv  17997  catcisolem  18017  mgmhmf1o  18574  xpsmnd  18651  mhmf1o  18670  xpsgrp  18938  ghmf1o  19127  symggrp  19279  symginv  19281  f1omvdcnv  19323  f1omvdconj  19325  pmtrfconj  19345  odngen  19456  gsumval3eu  19783  gsumval3  19786  gsumzf1o  19791  xpsrngd  20064  xpsringd  20217  fidomndrnglem  20657  lmhmf1o  20950  znleval  21461  zntoslem  21463  znunithash  21471  psrass1lem  21839  coe1sfi  22096  mdetleib2  22473  basqtop  23596  tgqtop  23597  reghmph  23678  indishmph  23683  cmphaushmeo  23685  ordthmeolem  23686  txhmeo  23688  xpstps  23695  xpstopnlem2  23696  qtopf1  23701  ufldom  23847  symgtgp  23991  tgpconncompeqg  23997  xpsdsfn  24263  xpsxmet  24266  xpsdsval  24267  xpsmet  24268  imasf1obl  24374  xpsxms  24420  xpsms  24421  iccpnfcnv  24840  xrhmeo  24842  ovoliunlem2  25402  vitalilem2  25508  mbfimaopnlem  25554  dvcnvlem  25878  dvcnv  25879  dvcnvrelem2  25921  dvcnvre  25922  efif1olem4  26452  eff1olem  26455  logrn  26465  logf1o  26471  dvlog  26558  asinrebnd  26809  sqff1o  27090  lgsqrlem4  27258  cnvmot  28486  f1otrg  28816  f1otrge  28817  cnvunop  31862  unopadj  31863  fresf1o  32574  fmptco1f1o  32576  padct  32662  fcobij  32664  fsumiunle  32774  ccatws1f1o  32893  mndlactf1o  32984  mndractf1o  32985  abliso  32990  gsumwrd2dccat  33020  symgcom  33025  tocycfvres1  33052  tocycfvres2  33053  cycpmcl  33058  cycpmconjvlem  33083  cycpmconjv  33084  cycpmconjslem1  33096  cycpmconjslem2  33097  cycpmconjs  33098  1arithidomlem2  33473  1arithidom  33474  madjusmdetlem2  33795  madjusmdetlem4  33797  tpr2rico  33879  esumiun  34061  reprpmtf1o  34594  derangenlem  35148  subfacp1lem4  35160  cvmfolem  35256  cvmliftlem6  35267  fv1stcnv  35754  fv2ndcnv  35755  f1ocan1fv  37710  f1ocan2fv  37711  ismtycnv  37786  ismtyima  37787  ismtyhmeolem  37788  ismtybndlem  37790  rngoisocnv  37965  lautcnv  40073  cdlemk45  40930  cdlemn9  41188  sticksstones18  42141  sticksstones19  42142  eldioph2  42739  kelac1  43040  brco2f1o  44009  brco3f1o  44010  sge0f1o  46367  3f1oss1  47063  3f1oss2  47064  grimcnv  47876  gricushgr  47905  isubgr3stgrlem7  47960  uspgrlimlem1  47976  uspgrlimlem2  47977  uspgrlimlem3  47978  grlicsym  48001