Theorem f1ocnv 6786

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 6594	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6147	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6583	. . . . . 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 6782	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6782	. 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 1541  ^◡ccnv 5623  Rel wrel 5629   Fn wfn 6487  –1-1-onto→wf1o 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  f1ocnvb  6787  f1orescnv  6789  f1imacnv  6790  f1cnv  6798  f1ococnv1  6803  f1oresrab  7072  f1ocnvfv2  7223  f1ocnvdm  7231  f1ocnvfvrneq  7232  fcof1oinvd  7239  fveqf1o  7248  isocnv  7276  weniso  7300  f1ofveu  7352  f1oexrnex  7869  f1oexbi  7870  fnwelem  8073  oacomf1o  8492  mapsnf1o3  8833  ener  8938  en0  8955  en0ALT  8956  en1  8961  omf1o  9008  domss2  9064  mapen  9069  ssenen  9079  f1oenfirn  9104  ensymfib  9108  snnen2o  9145  1sdom2dom  9154  infn0  9202  f1fi  9214  f1opwfi  9256  mapfienlem2  9309  mapfienlem3  9310  mapfien  9311  mapfien2  9312  ordiso2  9420  unxpwdom2  9493  cantnfle  9580  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1d  9597  cantnflem1  9598  wemapwe  9606  oef1o  9607  cnfcomlem  9608  cnfcom  9609  cnfcom2lem  9610  cnfcom2  9611  cnfcom3lem  9612  cnfcom3  9613  infxpenlem  9923  infxpenc  9928  dfac8b  9941  acndom  9961  acndom2  9964  iunfictbso  10024  dfac12lem2  10055  infpssrlem3  10215  infpssrlem4  10216  fin1a2lem7  10316  axcc3  10348  ttukeylem7  10425  fpwwe2lem5  10546  fpwwe2lem6  10547  pwfseqlem5  10574  axdc4uzlem  13906  seqf1olem1  13964  seqf1olem2  13965  hashfacen  14377  seqcoll  14387  seqcoll2  14388  cnrecnv  15088  isercolllem2  15589  isercoll  15591  summolem3  15637  summolem2a  15638  ackbijnn  15751  prodmolem3  15856  prodmolem2a  15857  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  sadaddlem  16393  sadasslem  16397  sadeq  16399  phimullem  16706  eulerthlem2  16709  unbenlem  16836  1arith2  16856  xpsbas  17493  xpsadd  17495  xpsmul  17496  xpssca  17497  xpsvsca  17498  xpsless  17499  xpsle  17500  setcinv  18014  catcisolem  18034  mgmhmf1o  18625  xpsmnd  18702  mhmf1o  18721  xpsgrp  18989  ghmf1o  19177  symggrp  19329  symginv  19331  f1omvdcnv  19373  f1omvdconj  19375  pmtrfconj  19395  odngen  19506  gsumval3eu  19833  gsumval3  19836  gsumzf1o  19841  xpsrngd  20114  xpsringd  20268  fidomndrnglem  20705  lmhmf1o  20998  znleval  21509  zntoslem  21511  znunithash  21519  psrass1lem  21888  coe1sfi  22154  mdetleib2  22532  basqtop  23655  tgqtop  23656  reghmph  23737  indishmph  23742  cmphaushmeo  23744  ordthmeolem  23745  txhmeo  23747  xpstps  23754  xpstopnlem2  23755  qtopf1  23760  ufldom  23906  symgtgp  24050  tgpconncompeqg  24056  xpsdsfn  24321  xpsxmet  24324  xpsdsval  24325  xpsmet  24326  imasf1obl  24432  xpsxms  24478  xpsms  24479  iccpnfcnv  24898  xrhmeo  24900  ovoliunlem2  25460  vitalilem2  25566  mbfimaopnlem  25612  dvcnvlem  25936  dvcnv  25937  dvcnvrelem2  25979  dvcnvre  25980  efif1olem4  26510  eff1olem  26513  logrn  26523  logf1o  26529  dvlog  26616  asinrebnd  26867  sqff1o  27148  lgsqrlem4  27316  oldfib  28373  cnvmot  28613  f1otrg  28943  f1otrge  28944  cnvunop  31993  unopadj  31994  fresf1o  32709  fmptco1f1o  32711  padct  32797  fcobij  32799  fsumiunle  32910  ccatws1f1o  33033  mndlactf1o  33112  mndractf1o  33113  abliso  33118  gsumwrd2dccat  33160  symgcom  33165  tocycfvres1  33192  tocycfvres2  33193  cycpmcl  33198  cycpmconjvlem  33223  cycpmconjv  33224  cycpmconjslem1  33236  cycpmconjslem2  33237  cycpmconjs  33238  1arithidomlem2  33617  1arithidom  33618  mplvrpmrhm  33712  esplysply  33729  madjusmdetlem2  33985  madjusmdetlem4  33987  tpr2rico  34069  esumiun  34251  reprpmtf1o  34783  derangenlem  35365  subfacp1lem4  35377  cvmfolem  35473  cvmliftlem6  35484  fv1stcnv  35971  fv2ndcnv  35972  f1ocan1fv  37927  f1ocan2fv  37928  ismtycnv  38003  ismtyima  38004  ismtyhmeolem  38005  ismtybndlem  38007  rngoisocnv  38182  lautcnv  40360  cdlemk45  41217  cdlemn9  41475  sticksstones18  42428  sticksstones19  42429  eldioph2  43014  kelac1  43315  brco2f1o  44283  brco3f1o  44284  sge0f1o  46636  3f1oss1  47331  3f1oss2  47332  grimcnv  48144  gricushgr  48173  isubgr3stgrlem7  48228  uspgrlimlem1  48244  uspgrlimlem2  48245  uspgrlimlem3  48246  grlicsym  48269