Theorem f1ocnv 6845

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 6649	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6186	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6638	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 251	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 220	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 39	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 628	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6841	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6841	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 295	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ^◡ccnv 5653  Rel wrel 5659   Fn wfn 6541  –1-1-onto→wf1o 6545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-br 5106  df-opab 5170  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553

This theorem is used by:  f1ocnvb  6846  f1orescnv  6848  f1imacnv  6849  f1cnv  6857  f1ococnv1  6862  f1oresrab  7136  f1ocnvfv2  7292  f1ocnvdm  7300  f1ocnvfvrneq  7301  fcof1oinvd  7308  fveqf1o  7317  isocnv  7345  weniso  7371  f1ofveu  7421  f1oexrnex  7946  f1oexbi  7947  fnwelem  8153  oacomf1o  8584  mapsnf1o3  8934  ener  9039  en0  9056  en0ALT  9057  en1  9062  omf1o  9110  domss2  9166  mapen  9171  ssenen  9181  f1oenfirn  9206  ensymfib  9210  snnen2o  9247  1sdom2dom  9256  infn0  9305  f1fi  9317  f1opwfi  9356  mapfienlem2  9408  mapfienlem3  9409  mapfien  9410  mapfien2  9411  ordiso2  9519  unxpwdom2  9592  cantnfle  9682  cantnfp1lem3  9691  cantnflem1b  9697  cantnflem1d  9699  cantnflem1  9700  wemapwe  9708  oef1o  9709  cnfcomlem  9710  cnfcom  9711  cnfcom2lem  9712  cnfcom2  9713  cnfcom3lem  9714  cnfcom3  9715  infxpenlem  10102  infxpenc  10107  dfac8b  10120  acndom  10140  acndom2  10143  iunfictbso  10203  dfac12lem2  10233  infpssrlem3  10393  infpssrlem4  10394  fin1a2lem7  10494  axcc3  10526  ttukeylem7  10603  fpwwe2lem5  10730  fpwwe2lem6  10731  pwfseqlem5  10758  axdc4uzlem  14136  seqf1olem1  14194  seqf1olem2  14195  hashfacen  14609  seqcoll  14619  seqcoll2  14620  cnrecnv  15344  isercolllem2  15845  isercoll  15847  summolem3  15892  summolem2a  15893  ackbijnn  16009  prodmolem3  16112  prodmolem2a  16113  sadcaddlem  16639  sadadd2lem  16641  sadadd3  16643  sadaddlem  16648  sadasslem  16652  sadeq  16654  phimullem  16968  eulerthlem2  16971  unbenlem  17098  1arith2  17118  xpsbas  17756  xpsadd  17758  xpsmul  17759  xpssca  17760  xpsvsca  17761  xpsless  17762  xpsle  17763  setcinv  18277  catcisolem  18297  mgmhmf1o  18901  xpsmnd  18983  mhmf1o  19003  xpsgrp  19281  ghmf1o  19474  symggrp  19626  symginv  19628  f1omvdcnv  19670  f1omvdconj  19672  pmtrfconj  19692  odngen  19803  gsumval3eu  20130  gsumval3  20133  gsumzf1o  20138  xpsrngd  20413  xpsringd  20574  fidomndrnglem  21042  lmhmf1o  21333  znleval  21872  zntoslem  21874  znunithash  21882  psrass1lem  22253  coe1sfi  22543  mdetleib2  22915  basqtop  24042  tgqtop  24043  reghmph  24124  indishmph  24129  cmphaushmeo  24131  ordthmeolem  24132  txhmeo  24134  xpstps  24141  xpstopnlem2  24142  qtopf1  24147  ufldom  24293  symgtgp  24437  tgpconncompeqg  24443  xpsdsfn  24708  xpsxmet  24711  xpsdsval  24712  xpsmet  24713  imasf1obl  24819  xpsxms  24865  xpsms  24866  iccpnfcnv  25277  xrhmeo  25279  ovoliunlem2  25836  vitalilem2  25942  mbfimaopnlem  25988  dvcnvlem  26308  dvcnv  26309  dvcnvrelem2  26350  dvcnvre  26351  efif1olem4  26885  eff1olem  26888  logrn  26898  logf1o  26904  dvlog  26991  asinrebnd  27241  sqff1o  27521  lgsqrlem4  27688  oldfib  28775  cnvmot  29016  f1otrg  29460  f1otrge  29461  cnvunop  32532  unopadj  32533  fresf1o  33279  fmptco1f1o  33281  padct  33364  fcobij  33365  fsumiunle  33473  ccatws1f1o  33567  mndlactf1o  33644  mndractf1o  33645  abliso  33649  gsumwrd2dccat  33692  symgcom  33697  tocycfvres1  33724  tocycfvres2  33725  cycpmcl  33730  cycpmconjvlem  33755  cycpmconjv  33756  cycpmconjslem1  33768  cycpmconjslem2  33769  cycpmconjs  33770  1arithidomlem2  34121  1arithidom  34122  mplvrpmrhm  34232  esplysply  34256  madjusmdetlem2  34513  madjusmdetlem4  34515  tpr2rico  34597  esumiun  34779  reprpmtf1o  35308  j0ltalephlem  35961  vonf1onprcf1ac  35998  prconf1acwevd  36002  onprcf1of1orad  36007  onprcf1of1orbd  36008  derangenlem  36057  subfacp1lem4  36069  cvmfolem  36165  cvmliftlem6  36176  fv1stcnv  36668  fv2ndcnv  36669  f1ocan1fv  38800  f1ocan2fv  38801  ismtycnv  38876  ismtyima  38877  ismtyhmeolem  38878  ismtybndlem  38880  rngoisocnv  39055  lautcnv  41287  cdlemk45  42144  cdlemn9  42402  sticksstones18  43354  sticksstones19  43355  eldioph2  43913  kelac1  44205  brco2f1o  45172  brco3f1o  45173  sge0f1o  47531  3f1oss1  48284  3f1oss2  48285  grimcnv  49125  gricushgr  49154  isubgr3stgrlem7  49209  uspgrlimlem1  49225  uspgrlimlem2  49226  uspgrlimlem3  49227  grlicsym  49250