Theorem f1ocnv 6819

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 6623	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6175	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6612	. . . . . 6 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
4	3	biimprd 250	. . . . 5 ⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
5	2, 4	sylbi 219	. . . 4 ⊢ (Rel 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴))
6	1, 5	mpcom 38	. . 3 ⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)
7	6	anim1ci 625	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6815	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6815	. 2 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
10	7, 8, 9	3imtr4i 294	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560  ^◡ccnv 5646  Rel wrel 5652   Fn wfn 6516  –1-1-onto→wf1o 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528

This theorem is referenced by:  f1ocnvb  6820  f1orescnv  6822  f1imacnv  6823  f1cnv  6831  f1ococnv1  6836  f1oresrab  7109  f1ocnvfv2  7261  f1ocnvdm  7269  f1ocnvfvrneq  7270  fcof1oinvd  7277  fveqf1o  7286  isocnv  7314  weniso  7338  f1ofveu  7390  f1oexrnex  7908  f1oexbi  7909  fnwelem  8111  oacomf1o  8534  mapsnf1o3  8877  ener  8982  en0  8999  en0ALT  9000  en1  9005  omf1o  9052  domss2  9108  mapen  9113  ssenen  9123  f1oenfirn  9148  ensymfib  9152  snnen2o  9189  1sdom2dom  9198  infn0  9246  f1fi  9258  f1opwfi  9299  mapfienlem2  9352  mapfienlem3  9353  mapfien  9354  mapfien2  9355  ordiso2  9463  unxpwdom2  9536  cantnfle  9626  cantnfp1lem3  9635  cantnflem1b  9641  cantnflem1d  9643  cantnflem1  9644  wemapwe  9652  oef1o  9653  cnfcomlem  9654  cnfcom  9655  cnfcom2lem  9656  cnfcom2  9657  cnfcom3lem  9658  cnfcom3  9659  infxpenlem  9969  infxpenc  9974  dfac8b  9987  acndom  10007  acndom2  10010  iunfictbso  10070  dfac12lem2  10101  infpssrlem3  10262  infpssrlem4  10263  fin1a2lem7  10363  axcc3  10395  ttukeylem7  10472  fpwwe2lem5  10593  fpwwe2lem6  10594  pwfseqlem5  10621  axdc4uzlem  13996  seqf1olem1  14054  seqf1olem2  14055  hashfacen  14467  seqcoll  14477  seqcoll2  14478  cnrecnv  15192  isercolllem2  15693  isercoll  15695  summolem3  15741  summolem2a  15742  ackbijnn  15858  prodmolem3  15963  prodmolem2a  15964  sadcaddlem  16491  sadadd2lem  16493  sadadd3  16495  sadaddlem  16500  sadasslem  16504  sadeq  16506  phimullem  16814  eulerthlem2  16817  unbenlem  16944  1arith2  16964  xpsbas  17602  xpsadd  17604  xpsmul  17605  xpssca  17606  xpsvsca  17607  xpsless  17608  xpsle  17609  setcinv  18123  catcisolem  18143  mgmhmf1o  18734  xpsmnd  18811  mhmf1o  18830  xpsgrp  19101  ghmf1o  19288  symggrp  19440  symginv  19442  f1omvdcnv  19484  f1omvdconj  19486  pmtrfconj  19506  odngen  19617  gsumval3eu  19944  gsumval3  19947  gsumzf1o  19952  xpsrngd  20225  xpsringd  20381  fidomndrnglem  20822  lmhmf1o  21113  znleval  21606  zntoslem  21608  znunithash  21616  psrass1lem  21985  coe1sfi  22275  mdetleib2  22648  basqtop  23771  tgqtop  23772  reghmph  23853  indishmph  23858  cmphaushmeo  23860  ordthmeolem  23861  txhmeo  23863  xpstps  23870  xpstopnlem2  23871  qtopf1  23876  ufldom  24022  symgtgp  24166  tgpconncompeqg  24172  xpsdsfn  24437  xpsxmet  24440  xpsdsval  24441  xpsmet  24442  imasf1obl  24548  xpsxms  24594  xpsms  24595  iccpnfcnv  25006  xrhmeo  25008  ovoliunlem2  25565  vitalilem2  25671  mbfimaopnlem  25717  dvcnvlem  26038  dvcnv  26039  dvcnvrelem2  26080  dvcnvre  26081  efif1olem4  26610  eff1olem  26613  logrn  26623  logf1o  26629  dvlog  26716  asinrebnd  26966  sqff1o  27246  lgsqrlem4  27413  oldfib  28470  cnvmot  28710  f1otrg  29071  f1otrge  29072  cnvunop  32121  unopadj  32122  fresf1o  32833  fmptco1f1o  32835  padct  32920  fcobij  32922  fsumiunle  33031  ccatws1f1o  33129  mndlactf1o  33208  mndractf1o  33209  abliso  33214  gsumwrd2dccat  33258  symgcom  33263  tocycfvres1  33290  tocycfvres2  33291  cycpmcl  33296  cycpmconjvlem  33321  cycpmconjv  33322  cycpmconjslem1  33334  cycpmconjslem2  33335  cycpmconjs  33336  1arithidomlem2  33732  1arithidom  33733  mplvrpmrhm  33844  esplysply  33868  madjusmdetlem2  34125  madjusmdetlem4  34127  tpr2rico  34209  esumiun  34391  reprpmtf1o  34920  derangenlem  35521  subfacp1lem4  35533  cvmfolem  35629  cvmliftlem6  35640  fv1stcnv  36127  fv2ndcnv  36128  f1ocan1fv  38225  f1ocan2fv  38226  ismtycnv  38301  ismtyima  38302  ismtyhmeolem  38303  ismtybndlem  38305  rngoisocnv  38480  lautcnv  40714  cdlemk45  41571  cdlemn9  41829  sticksstones18  42781  sticksstones19  42782  eldioph2  43343  kelac1  43640  brco2f1o  44608  brco3f1o  44609  sge0f1o  46956  3f1oss1  47669  3f1oss2  47670  grimcnv  48510  gricushgr  48539  isubgr3stgrlem7  48594  uspgrlimlem1  48610  uspgrlimlem2  48611  uspgrlimlem3  48612  grlicsym  48635