Theorem f1ocnv 6831

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 6635	. . . 4 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel2 6182	. . . . 5 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹)
3		fneq1 6624	. . . . . 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 6827	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
9		dff1o4 6827	. 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 1570  ^◡ccnv 5654  Rel wrel 5660   Fn wfn 6528  –1-1-onto→wf1o 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540

This theorem is used by:  f1ocnvb  6832  f1orescnv  6834  f1imacnv  6835  f1cnv  6843  f1ococnv1  6848  f1oresrab  7122  f1ocnvfv2  7279  f1ocnvdm  7287  f1ocnvfvrneq  7288  fcof1oinvd  7295  fveqf1o  7304  isocnv  7332  weniso  7358  f1ofveu  7408  f1oexrnex  7925  f1oexbi  7926  fnwelem  8130  oacomf1o  8553  mapsnf1o3  8903  ener  9008  en0  9025  en0ALT  9026  en1  9031  omf1o  9079  domss2  9135  mapen  9140  ssenen  9150  f1oenfirn  9175  ensymfib  9179  snnen2o  9216  1sdom2dom  9225  infn0  9273  f1fi  9285  f1opwfi  9324  mapfienlem2  9377  mapfienlem3  9378  mapfien  9379  mapfien2  9380  ordiso2  9488  unxpwdom2  9561  cantnfle  9651  cantnfp1lem3  9660  cantnflem1b  9666  cantnflem1d  9668  cantnflem1  9669  wemapwe  9677  oef1o  9678  cnfcomlem  9679  cnfcom  9680  cnfcom2lem  9681  cnfcom2  9682  cnfcom3lem  9683  cnfcom3  9684  infxpenlem  10017  infxpenc  10022  dfac8b  10035  acndom  10055  acndom2  10058  iunfictbso  10118  dfac12lem2  10148  infpssrlem3  10308  infpssrlem4  10309  fin1a2lem7  10409  axcc3  10441  ttukeylem7  10518  fpwwe2lem5  10645  fpwwe2lem6  10646  pwfseqlem5  10673  axdc4uzlem  14048  seqf1olem1  14106  seqf1olem2  14107  hashfacen  14520  seqcoll  14530  seqcoll2  14531  cnrecnv  15253  isercolllem2  15754  isercoll  15756  summolem3  15801  summolem2a  15802  ackbijnn  15918  prodmolem3  16021  prodmolem2a  16022  sadcaddlem  16548  sadadd2lem  16550  sadadd3  16552  sadaddlem  16557  sadasslem  16561  sadeq  16563  phimullem  16871  eulerthlem2  16874  unbenlem  17001  1arith2  17021  xpsbas  17659  xpsadd  17661  xpsmul  17662  xpssca  17663  xpsvsca  17664  xpsless  17665  xpsle  17666  setcinv  18180  catcisolem  18200  mgmhmf1o  18803  xpsmnd  18885  mhmf1o  18905  xpsgrp  19183  ghmf1o  19376  symggrp  19528  symginv  19530  f1omvdcnv  19572  f1omvdconj  19574  pmtrfconj  19594  odngen  19705  gsumval3eu  20032  gsumval3  20035  gsumzf1o  20040  xpsrngd  20315  xpsringd  20474  fidomndrnglem  20940  lmhmf1o  21231  znleval  21768  zntoslem  21770  znunithash  21778  psrass1lem  22149  coe1sfi  22439  mdetleib2  22811  basqtop  23938  tgqtop  23939  reghmph  24020  indishmph  24025  cmphaushmeo  24027  ordthmeolem  24028  txhmeo  24030  xpstps  24037  xpstopnlem2  24038  qtopf1  24043  ufldom  24189  symgtgp  24333  tgpconncompeqg  24339  xpsdsfn  24604  xpsxmet  24607  xpsdsval  24608  xpsmet  24609  imasf1obl  24715  xpsxms  24761  xpsms  24762  iccpnfcnv  25173  xrhmeo  25175  ovoliunlem2  25732  vitalilem2  25838  mbfimaopnlem  25884  dvcnvlem  26204  dvcnv  26205  dvcnvrelem2  26246  dvcnvre  26247  efif1olem4  26783  eff1olem  26786  logrn  26796  logf1o  26802  dvlog  26889  asinrebnd  27139  sqff1o  27419  lgsqrlem4  27586  oldfib  28643  cnvmot  28884  f1otrg  29328  f1otrge  29329  cnvunop  32400  unopadj  32401  fresf1o  33105  fmptco1f1o  33107  padct  33190  fcobij  33192  fsumiunle  33300  ccatws1f1o  33394  mndlactf1o  33471  mndractf1o  33472  abliso  33476  gsumwrd2dccat  33519  symgcom  33524  tocycfvres1  33551  tocycfvres2  33552  cycpmcl  33557  cycpmconjvlem  33582  cycpmconjv  33583  cycpmconjslem1  33595  cycpmconjslem2  33596  cycpmconjs  33597  1arithidomlem2  33947  1arithidom  33948  mplvrpmrhm  34058  esplysply  34082  madjusmdetlem2  34339  madjusmdetlem4  34341  tpr2rico  34423  esumiun  34605  reprpmtf1o  35135  derangenlem  35751  subfacp1lem4  35763  cvmfolem  35859  cvmliftlem6  35870  fv1stcnv  36357  fv2ndcnv  36358  f1ocan1fv  38477  f1ocan2fv  38478  ismtycnv  38553  ismtyima  38554  ismtyhmeolem  38555  ismtybndlem  38557  rngoisocnv  38732  lautcnv  40964  cdlemk45  41821  cdlemn9  42079  sticksstones18  43031  sticksstones19  43032  eldioph2  43608  kelac1  43905  brco2f1o  44873  brco3f1o  44874  sge0f1o  47211  3f1oss1  47964  3f1oss2  47965  grimcnv  48805  gricushgr  48834  isubgr3stgrlem7  48889  uspgrlimlem1  48905  uspgrlimlem2  48906  uspgrlimlem3  48907  grlicsym  48930