Theorem f1ocnv 6796

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 6604	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6157	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6593	. . . . . 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 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6792	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6792	. 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 1542  ^◡ccnv 5633  Rel wrel 5639   Fn wfn 6497  –1-1-onto→wf1o 6501

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509

This theorem is referenced by:  f1ocnvb  6797  f1orescnv  6799  f1imacnv  6800  f1cnv  6808  f1ococnv1  6813  f1oresrab  7084  f1ocnvfv2  7235  f1ocnvdm  7243  f1ocnvfvrneq  7244  fcof1oinvd  7251  fveqf1o  7260  isocnv  7288  weniso  7312  f1ofveu  7364  f1oexrnex  7881  f1oexbi  7882  fnwelem  8085  oacomf1o  8504  mapsnf1o3  8847  ener  8952  en0  8969  en0ALT  8970  en1  8975  omf1o  9022  domss2  9078  mapen  9083  ssenen  9093  f1oenfirn  9118  ensymfib  9122  snnen2o  9159  1sdom2dom  9168  infn0  9216  f1fi  9228  f1opwfi  9270  mapfienlem2  9323  mapfienlem3  9324  mapfien  9325  mapfien2  9326  ordiso2  9434  unxpwdom2  9507  cantnfle  9594  cantnfp1lem3  9603  cantnflem1b  9609  cantnflem1d  9611  cantnflem1  9612  wemapwe  9620  oef1o  9621  cnfcomlem  9622  cnfcom  9623  cnfcom2lem  9624  cnfcom2  9625  cnfcom3lem  9626  cnfcom3  9627  infxpenlem  9937  infxpenc  9942  dfac8b  9955  acndom  9975  acndom2  9978  iunfictbso  10038  dfac12lem2  10069  infpssrlem3  10229  infpssrlem4  10230  fin1a2lem7  10330  axcc3  10362  ttukeylem7  10439  fpwwe2lem5  10560  fpwwe2lem6  10561  pwfseqlem5  10588  axdc4uzlem  13920  seqf1olem1  13978  seqf1olem2  13979  hashfacen  14391  seqcoll  14401  seqcoll2  14402  cnrecnv  15102  isercolllem2  15603  isercoll  15605  summolem3  15651  summolem2a  15652  ackbijnn  15765  prodmolem3  15870  prodmolem2a  15871  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  sadaddlem  16407  sadasslem  16411  sadeq  16413  phimullem  16720  eulerthlem2  16723  unbenlem  16850  1arith2  16870  xpsbas  17507  xpsadd  17509  xpsmul  17510  xpssca  17511  xpsvsca  17512  xpsless  17513  xpsle  17514  setcinv  18028  catcisolem  18048  mgmhmf1o  18639  xpsmnd  18716  mhmf1o  18735  xpsgrp  19006  ghmf1o  19194  symggrp  19346  symginv  19348  f1omvdcnv  19390  f1omvdconj  19392  pmtrfconj  19412  odngen  19523  gsumval3eu  19850  gsumval3  19853  gsumzf1o  19858  xpsrngd  20131  xpsringd  20285  fidomndrnglem  20722  lmhmf1o  21015  znleval  21526  zntoslem  21528  znunithash  21536  psrass1lem  21905  coe1sfi  22171  mdetleib2  22549  basqtop  23672  tgqtop  23673  reghmph  23754  indishmph  23759  cmphaushmeo  23761  ordthmeolem  23762  txhmeo  23764  xpstps  23771  xpstopnlem2  23772  qtopf1  23777  ufldom  23923  symgtgp  24067  tgpconncompeqg  24073  xpsdsfn  24338  xpsxmet  24341  xpsdsval  24342  xpsmet  24343  imasf1obl  24449  xpsxms  24495  xpsms  24496  iccpnfcnv  24915  xrhmeo  24917  ovoliunlem2  25477  vitalilem2  25583  mbfimaopnlem  25629  dvcnvlem  25953  dvcnv  25954  dvcnvrelem2  25996  dvcnvre  25997  efif1olem4  26527  eff1olem  26530  logrn  26540  logf1o  26546  dvlog  26633  asinrebnd  26884  sqff1o  27165  lgsqrlem4  27333  oldfib  28390  cnvmot  28631  f1otrg  28961  f1otrge  28962  cnvunop  32012  unopadj  32013  fresf1o  32727  fmptco1f1o  32729  padct  32814  fcobij  32816  fsumiunle  32927  ccatws1f1o  33050  mndlactf1o  33129  mndractf1o  33130  abliso  33135  gsumwrd2dccat  33178  symgcom  33183  tocycfvres1  33210  tocycfvres2  33211  cycpmcl  33216  cycpmconjvlem  33241  cycpmconjv  33242  cycpmconjslem1  33254  cycpmconjslem2  33255  cycpmconjs  33256  1arithidomlem2  33635  1arithidom  33636  mplvrpmrhm  33730  esplysply  33754  madjusmdetlem2  34012  madjusmdetlem4  34014  tpr2rico  34096  esumiun  34278  reprpmtf1o  34810  derangenlem  35393  subfacp1lem4  35405  cvmfolem  35501  cvmliftlem6  35512  fv1stcnv  35999  fv2ndcnv  36000  f1ocan1fv  38006  f1ocan2fv  38007  ismtycnv  38082  ismtyima  38083  ismtyhmeolem  38084  ismtybndlem  38086  rngoisocnv  38261  lautcnv  40495  cdlemk45  41352  cdlemn9  41610  sticksstones18  42563  sticksstones19  42564  eldioph2  43148  kelac1  43449  brco2f1o  44417  brco3f1o  44418  sge0f1o  46769  3f1oss1  47464  3f1oss2  47465  grimcnv  48277  gricushgr  48306  isubgr3stgrlem7  48361  uspgrlimlem1  48377  uspgrlimlem2  48378  uspgrlimlem3  48379  grlicsym  48402