Theorem f1ocnv 6792

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 6600	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6153	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6589	. . . . . 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 617	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴))
8		dff1o4 6788	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6788	. 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 1542  ^◡ccnv 5630  Rel wrel 5636   Fn wfn 6493  –1-1-onto→wf1o 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1ocnvb  6793  f1orescnv  6795  f1imacnv  6796  f1cnv  6804  f1ococnv1  6809  f1oresrab  7080  f1ocnvfv2  7232  f1ocnvdm  7240  f1ocnvfvrneq  7241  fcof1oinvd  7248  fveqf1o  7257  isocnv  7285  weniso  7309  f1ofveu  7361  f1oexrnex  7878  f1oexbi  7879  fnwelem  8081  oacomf1o  8500  mapsnf1o3  8843  ener  8948  en0  8965  en0ALT  8966  en1  8971  omf1o  9018  domss2  9074  mapen  9079  ssenen  9089  f1oenfirn  9114  ensymfib  9118  snnen2o  9155  1sdom2dom  9164  infn0  9212  f1fi  9224  f1opwfi  9266  mapfienlem2  9319  mapfienlem3  9320  mapfien  9321  mapfien2  9322  ordiso2  9430  unxpwdom2  9503  cantnfle  9592  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  wemapwe  9618  oef1o  9619  cnfcomlem  9620  cnfcom  9621  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  infxpenlem  9935  infxpenc  9940  dfac8b  9953  acndom  9973  acndom2  9976  iunfictbso  10036  dfac12lem2  10067  infpssrlem3  10227  infpssrlem4  10228  fin1a2lem7  10328  axcc3  10360  ttukeylem7  10437  fpwwe2lem5  10558  fpwwe2lem6  10559  pwfseqlem5  10586  axdc4uzlem  13945  seqf1olem1  14003  seqf1olem2  14004  hashfacen  14416  seqcoll  14426  seqcoll2  14427  cnrecnv  15127  isercolllem2  15628  isercoll  15630  summolem3  15676  summolem2a  15677  ackbijnn  15793  prodmolem3  15898  prodmolem2a  15899  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  sadaddlem  16435  sadasslem  16439  sadeq  16441  phimullem  16749  eulerthlem2  16752  unbenlem  16879  1arith2  16899  xpsbas  17536  xpsadd  17538  xpsmul  17539  xpssca  17540  xpsvsca  17541  xpsless  17542  xpsle  17543  setcinv  18057  catcisolem  18077  mgmhmf1o  18668  xpsmnd  18745  mhmf1o  18764  xpsgrp  19035  ghmf1o  19223  symggrp  19375  symginv  19377  f1omvdcnv  19419  f1omvdconj  19421  pmtrfconj  19441  odngen  19552  gsumval3eu  19879  gsumval3  19882  gsumzf1o  19887  xpsrngd  20160  xpsringd  20312  fidomndrnglem  20749  lmhmf1o  21041  znleval  21534  zntoslem  21536  znunithash  21544  psrass1lem  21912  coe1sfi  22177  mdetleib2  22553  basqtop  23676  tgqtop  23677  reghmph  23758  indishmph  23763  cmphaushmeo  23765  ordthmeolem  23766  txhmeo  23768  xpstps  23775  xpstopnlem2  23776  qtopf1  23781  ufldom  23927  symgtgp  24071  tgpconncompeqg  24077  xpsdsfn  24342  xpsxmet  24345  xpsdsval  24346  xpsmet  24347  imasf1obl  24453  xpsxms  24499  xpsms  24500  iccpnfcnv  24911  xrhmeo  24913  ovoliunlem2  25470  vitalilem2  25576  mbfimaopnlem  25622  dvcnvlem  25943  dvcnv  25944  dvcnvrelem2  25985  dvcnvre  25986  efif1olem4  26509  eff1olem  26512  logrn  26522  logf1o  26528  dvlog  26615  asinrebnd  26865  sqff1o  27145  lgsqrlem4  27312  oldfib  28369  cnvmot  28609  f1otrg  28939  f1otrge  28940  cnvunop  31989  unopadj  31990  fresf1o  32704  fmptco1f1o  32706  padct  32791  fcobij  32793  fsumiunle  32902  ccatws1f1o  33011  mndlactf1o  33090  mndractf1o  33091  abliso  33096  gsumwrd2dccat  33139  symgcom  33144  tocycfvres1  33171  tocycfvres2  33172  cycpmcl  33177  cycpmconjvlem  33202  cycpmconjv  33203  cycpmconjslem1  33215  cycpmconjslem2  33216  cycpmconjs  33217  1arithidomlem2  33596  1arithidom  33597  mplvrpmrhm  33691  esplysply  33715  madjusmdetlem2  33972  madjusmdetlem4  33974  tpr2rico  34056  esumiun  34238  reprpmtf1o  34770  derangenlem  35353  subfacp1lem4  35365  cvmfolem  35461  cvmliftlem6  35472  fv1stcnv  35959  fv2ndcnv  35960  f1ocan1fv  38047  f1ocan2fv  38048  ismtycnv  38123  ismtyima  38124  ismtyhmeolem  38125  ismtybndlem  38127  rngoisocnv  38302  lautcnv  40536  cdlemk45  41393  cdlemn9  41651  sticksstones18  42603  sticksstones19  42604  eldioph2  43194  kelac1  43491  brco2f1o  44459  brco3f1o  44460  sge0f1o  46810  3f1oss1  47523  3f1oss2  47524  grimcnv  48364  gricushgr  48393  isubgr3stgrlem7  48448  uspgrlimlem1  48464  uspgrlimlem2  48465  uspgrlimlem3  48466  grlicsym  48489