Theorem f1ocnv 6643

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 6450	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6031	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6440	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 251	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 220	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 619	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6639	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6639	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 295	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1542  ^◡ccnv 5534  Rel wrel 5540   Fn wfn 6345  –1-1-onto→wf1o 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-br 5041  df-opab 5103  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357

This theorem is referenced by:  f1ocnvb  6644  f1orescnv  6646  f1imacnv  6647  f1cnv  6654  f1ococnv1  6659  f1oresrab  6912  f1ocnvfv2  7058  f1ocnvdm  7065  f1ocnvfvrneq  7066  fcof1oinvd  7073  fveqf1o  7083  isocnv  7109  weniso  7133  f1ofveu  7178  f1oexrnex  7671  f1oexbi  7672  fnwelem  7864  oacomf1o  8235  mapsnf1o3  8518  ener  8615  en0  8631  en0OLD  8632  en1  8636  omf1o  8682  domss2  8739  mapen  8744  ssenen  8754  f1oenfirn  8793  ensymfib  8795  f1fi  8897  f1opwfi  8914  mapfienlem2  8956  mapfienlem3  8957  mapfien  8958  mapfien2  8959  ordiso2  9065  unxpwdom2  9138  cantnfle  9220  cantnfp1lem3  9229  cantnflem1b  9235  cantnflem1d  9237  cantnflem1  9238  wemapwe  9246  oef1o  9247  cnfcomlem  9248  cnfcom  9249  cnfcom2lem  9250  cnfcom2  9251  cnfcom3lem  9252  cnfcom3  9253  infxpenlem  9526  infxpenc  9531  dfac8b  9544  acndom  9564  acndom2  9567  iunfictbso  9627  dfac12lem2  9657  infpssrlem3  9818  infpssrlem4  9819  fin1a2lem7  9919  axcc3  9951  ttukeylem7  10028  fpwwe2lem5  10148  fpwwe2lem6  10149  pwfseqlem5  10176  axdc4uzlem  13455  seqf1olem1  13514  seqf1olem2  13515  hashfacen  13917  hashfacenOLD  13918  seqcoll  13929  seqcoll2  13930  cnrecnv  14627  isercolllem2  15128  isercoll  15130  summolem3  15177  summolem2a  15178  ackbijnn  15289  prodmolem3  15392  prodmolem2a  15393  sadcaddlem  15913  sadadd2lem  15915  sadadd3  15917  sadaddlem  15922  sadasslem  15926  sadeq  15928  phimullem  16229  eulerthlem2  16232  unbenlem  16357  1arith2  16377  xpsbas  16961  xpsadd  16963  xpsmul  16964  xpssca  16965  xpsvsca  16966  xpsless  16967  xpsle  16968  setcinv  17475  catcisolem  17495  xpsmnd  18080  mhmf1o  18095  xpsgrp  18349  ghmf1o  18519  symggrp  18659  symginv  18661  f1omvdcnv  18703  f1omvdconj  18705  pmtrfconj  18725  odngen  18833  gsumval3eu  19156  gsumval3  19159  gsumzf1o  19164  lmhmf1o  19950  fidomndrnglem  20211  znleval  20386  zntoslem  20388  znunithash  20396  psrass1lemOLD  20766  psrass1lem  20769  coe1sfi  21001  mdetleib2  21352  basqtop  22475  tgqtop  22476  reghmph  22557  indishmph  22562  cmphaushmeo  22564  ordthmeolem  22565  txhmeo  22567  xpstps  22574  xpstopnlem2  22575  qtopf1  22580  ufldom  22726  symgtgp  22870  tgpconncompeqg  22876  xpsdsfn  23143  xpsxmet  23146  xpsdsval  23147  xpsmet  23148  imasf1obl  23254  xpsxms  23300  xpsms  23301  iccpnfcnv  23709  xrhmeo  23711  ovoliunlem2  24268  vitalilem2  24374  mbfimaopnlem  24420  dvcnvlem  24741  dvcnv  24742  dvcnvrelem2  24783  dvcnvre  24784  efif1olem4  25302  eff1olem  25305  logrn  25315  logf1o  25321  dvlog  25407  asinrebnd  25652  sqff1o  25932  lgsqrlem4  26098  cnvmot  26500  f1otrg  26830  f1otrge  26831  cnvunop  29866  unopadj  29867  fresf1o  30553  fmptco1f1o  30555  padct  30642  fcobij  30645  fsumiunle  30731  abliso  30895  symgcom  30942  tocycfvres1  30967  tocycfvres2  30968  cycpmcl  30973  cycpmconjvlem  30998  cycpmconjv  30999  cycpmconjslem1  31011  cycpmconjslem2  31012  cycpmconjs  31013  madjusmdetlem2  31363  madjusmdetlem4  31365  tpr2rico  31447  esumiun  31645  reprpmtf1o  32189  derangenlem  32717  subfacp1lem4  32729  cvmfolem  32825  cvmliftlem6  32836  fv1stcnv  33338  fv2ndcnv  33339  f1ocan1fv  35540  f1ocan2fv  35541  ismtycnv  35616  ismtyima  35617  ismtyhmeolem  35618  ismtybndlem  35620  rngoisocnv  35795  lautcnv  37760  cdlemk45  38617  cdlemn9  38875  metakunt34  39790  eldioph2  40197  kelac1  40501  brco2f1o  41229  brco3f1o  41230  sge0f1o  43503  isomushgr  44860  isomgrsym  44870  mgmhmf1o  44923