Theorem f1ocnv 6812

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 6620	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6162	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6609	. . . . . 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 6808	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6808	. 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 5637  Rel wrel 5643   Fn wfn 6506  –1-1-onto→wf1o 6510

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1ocnvb  6813  f1orescnv  6815  f1imacnv  6816  f1cnv  6824  f1ococnv1  6829  f1oresrab  7099  f1ocnvfv2  7252  f1ocnvdm  7260  f1ocnvfvrneq  7261  fcof1oinvd  7268  fveqf1o  7277  isocnv  7305  weniso  7329  f1ofveu  7381  f1oexrnex  7903  f1oexbi  7904  fnwelem  8110  oacomf1o  8529  mapsnf1o3  8868  ener  8972  en0  8989  en0ALT  8990  en1  8995  omf1o  9044  domss2  9100  mapen  9105  ssenen  9115  f1oenfirn  9144  ensymfib  9148  snnen2o  9184  1sdom2dom  9194  infn0  9251  f1fi  9263  f1opwfi  9307  mapfienlem2  9357  mapfienlem3  9358  mapfien  9359  mapfien2  9360  ordiso2  9468  unxpwdom2  9541  cantnfle  9624  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1d  9641  cantnflem1  9642  wemapwe  9650  oef1o  9651  cnfcomlem  9652  cnfcom  9653  cnfcom2lem  9654  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  infxpenlem  9966  infxpenc  9971  dfac8b  9984  acndom  10004  acndom2  10007  iunfictbso  10067  dfac12lem2  10098  infpssrlem3  10258  infpssrlem4  10259  fin1a2lem7  10359  axcc3  10391  ttukeylem7  10468  fpwwe2lem5  10588  fpwwe2lem6  10589  pwfseqlem5  10616  axdc4uzlem  13948  seqf1olem1  14006  seqf1olem2  14007  hashfacen  14419  seqcoll  14429  seqcoll2  14430  cnrecnv  15131  isercolllem2  15632  isercoll  15634  summolem3  15680  summolem2a  15681  ackbijnn  15794  prodmolem3  15899  prodmolem2a  15900  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  phimullem  16749  eulerthlem2  16752  unbenlem  16879  1arith2  16899  xpsbas  17535  xpsadd  17537  xpsmul  17538  xpssca  17539  xpsvsca  17540  xpsless  17541  xpsle  17542  setcinv  18052  catcisolem  18072  mgmhmf1o  18627  xpsmnd  18704  mhmf1o  18723  xpsgrp  18991  ghmf1o  19180  symggrp  19330  symginv  19332  f1omvdcnv  19374  f1omvdconj  19376  pmtrfconj  19396  odngen  19507  gsumval3eu  19834  gsumval3  19837  gsumzf1o  19842  xpsrngd  20088  xpsringd  20241  fidomndrnglem  20681  lmhmf1o  20953  znleval  21464  zntoslem  21466  znunithash  21474  psrass1lem  21841  coe1sfi  22098  mdetleib2  22475  basqtop  23598  tgqtop  23599  reghmph  23680  indishmph  23685  cmphaushmeo  23687  ordthmeolem  23688  txhmeo  23690  xpstps  23697  xpstopnlem2  23698  qtopf1  23703  ufldom  23849  symgtgp  23993  tgpconncompeqg  23999  xpsdsfn  24265  xpsxmet  24268  xpsdsval  24269  xpsmet  24270  imasf1obl  24376  xpsxms  24422  xpsms  24423  iccpnfcnv  24842  xrhmeo  24844  ovoliunlem2  25404  vitalilem2  25510  mbfimaopnlem  25556  dvcnvlem  25880  dvcnv  25881  dvcnvrelem2  25923  dvcnvre  25924  efif1olem4  26454  eff1olem  26457  logrn  26467  logf1o  26473  dvlog  26560  asinrebnd  26811  sqff1o  27092  lgsqrlem4  27260  cnvmot  28468  f1otrg  28798  f1otrge  28799  cnvunop  31847  unopadj  31848  fresf1o  32555  fmptco1f1o  32557  padct  32643  fcobij  32645  fsumiunle  32754  ccatws1f1o  32873  mndlactf1o  32971  mndractf1o  32972  abliso  32977  gsumwrd2dccat  33007  symgcom  33040  tocycfvres1  33067  tocycfvres2  33068  cycpmcl  33073  cycpmconjvlem  33098  cycpmconjv  33099  cycpmconjslem1  33111  cycpmconjslem2  33112  cycpmconjs  33113  1arithidomlem2  33507  1arithidom  33508  madjusmdetlem2  33818  madjusmdetlem4  33820  tpr2rico  33902  esumiun  34084  reprpmtf1o  34617  derangenlem  35158  subfacp1lem4  35170  cvmfolem  35266  cvmliftlem6  35277  fv1stcnv  35764  fv2ndcnv  35765  f1ocan1fv  37720  f1ocan2fv  37721  ismtycnv  37796  ismtyima  37797  ismtyhmeolem  37798  ismtybndlem  37800  rngoisocnv  37975  lautcnv  40084  cdlemk45  40941  cdlemn9  41199  sticksstones18  42152  sticksstones19  42153  eldioph2  42750  kelac1  43052  brco2f1o  44021  brco3f1o  44022  sge0f1o  46380  3f1oss1  47076  3f1oss2  47077  grimcnv  47888  gricushgr  47917  isubgr3stgrlem7  47971  uspgrlimlem1  47987  uspgrlimlem2  47988  uspgrlimlem3  47989  grlicsym  48005