Theorem f1ocnv 6712

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 6519	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6081	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6508	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 247	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 216	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 615	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6708	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6708	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 291	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ^◡ccnv 5579  Rel wrel 5585   Fn wfn 6413  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1ocnvb  6713  f1orescnv  6715  f1imacnv  6716  f1cnv  6723  f1ococnv1  6728  f1oresrab  6981  f1ocnvfv2  7130  f1ocnvdm  7137  f1ocnvfvrneq  7138  fcof1oinvd  7145  fveqf1o  7155  isocnv  7181  weniso  7205  f1ofveu  7250  f1oexrnex  7748  f1oexbi  7749  fnwelem  7943  oacomf1o  8358  mapsnf1o3  8641  ener  8742  en0  8758  en0OLD  8759  en0ALT  8760  en1  8765  en1OLD  8766  omf1o  8815  domss2  8872  mapen  8877  ssenen  8887  f1oenfirn  8927  ensymfib  8930  f1fi  9036  f1opwfi  9053  mapfienlem2  9095  mapfienlem3  9096  mapfien  9097  mapfien2  9098  ordiso2  9204  unxpwdom2  9277  cantnfle  9359  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1d  9376  cantnflem1  9377  wemapwe  9385  oef1o  9386  cnfcomlem  9387  cnfcom  9388  cnfcom2lem  9389  cnfcom2  9390  cnfcom3lem  9391  cnfcom3  9392  infxpenlem  9700  infxpenc  9705  dfac8b  9718  acndom  9738  acndom2  9741  iunfictbso  9801  dfac12lem2  9831  infpssrlem3  9992  infpssrlem4  9993  fin1a2lem7  10093  axcc3  10125  ttukeylem7  10202  fpwwe2lem5  10322  fpwwe2lem6  10323  pwfseqlem5  10350  axdc4uzlem  13631  seqf1olem1  13690  seqf1olem2  13691  hashfacen  14094  hashfacenOLD  14095  seqcoll  14106  seqcoll2  14107  cnrecnv  14804  isercolllem2  15305  isercoll  15307  summolem3  15354  summolem2a  15355  ackbijnn  15468  prodmolem3  15571  prodmolem2a  15572  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  phimullem  16408  eulerthlem2  16411  unbenlem  16537  1arith2  16557  xpsbas  17200  xpsadd  17202  xpsmul  17203  xpssca  17204  xpsvsca  17205  xpsless  17206  xpsle  17207  setcinv  17721  catcisolem  17741  xpsmnd  18340  mhmf1o  18355  xpsgrp  18609  ghmf1o  18779  symggrp  18923  symginv  18925  f1omvdcnv  18967  f1omvdconj  18969  pmtrfconj  18989  odngen  19097  gsumval3eu  19420  gsumval3  19423  gsumzf1o  19428  lmhmf1o  20223  fidomndrnglem  20491  znleval  20674  zntoslem  20676  znunithash  20684  psrass1lemOLD  21053  psrass1lem  21056  coe1sfi  21294  mdetleib2  21645  basqtop  22770  tgqtop  22771  reghmph  22852  indishmph  22857  cmphaushmeo  22859  ordthmeolem  22860  txhmeo  22862  xpstps  22869  xpstopnlem2  22870  qtopf1  22875  ufldom  23021  symgtgp  23165  tgpconncompeqg  23171  xpsdsfn  23438  xpsxmet  23441  xpsdsval  23442  xpsmet  23443  imasf1obl  23550  xpsxms  23596  xpsms  23597  iccpnfcnv  24013  xrhmeo  24015  ovoliunlem2  24572  vitalilem2  24678  mbfimaopnlem  24724  dvcnvlem  25045  dvcnv  25046  dvcnvrelem2  25087  dvcnvre  25088  efif1olem4  25606  eff1olem  25609  logrn  25619  logf1o  25625  dvlog  25711  asinrebnd  25956  sqff1o  26236  lgsqrlem4  26402  cnvmot  26806  f1otrg  27136  f1otrge  27137  cnvunop  30181  unopadj  30182  fresf1o  30867  fmptco1f1o  30869  padct  30956  fcobij  30959  fsumiunle  31045  abliso  31207  symgcom  31254  tocycfvres1  31279  tocycfvres2  31280  cycpmcl  31285  cycpmconjvlem  31310  cycpmconjv  31311  cycpmconjslem1  31323  cycpmconjslem2  31324  cycpmconjs  31325  madjusmdetlem2  31680  madjusmdetlem4  31682  tpr2rico  31764  esumiun  31962  reprpmtf1o  32506  derangenlem  33033  subfacp1lem4  33045  cvmfolem  33141  cvmliftlem6  33152  fv1stcnv  33657  fv2ndcnv  33658  f1ocan1fv  35811  f1ocan2fv  35812  ismtycnv  35887  ismtyima  35888  ismtyhmeolem  35889  ismtybndlem  35891  rngoisocnv  36066  lautcnv  38031  cdlemk45  38888  cdlemn9  39146  sticksstones18  40048  sticksstones19  40049  metakunt34  40086  eldioph2  40500  kelac1  40804  brco2f1o  41531  brco3f1o  41532  sge0f1o  43810  isomushgr  45166  isomgrsym  45176  mgmhmf1o  45229