Theorem f1ocnv 6149

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	|- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )

Proof of Theorem f1ocnv

Step	Hyp	Ref	Expression
1		fnrel 5989	. . . . 5 |- ( F Fn A -> Rel F )
2		dfrel2 5583	. . . . . 6 |- ( Rel F <-> `' `' F = F )
3		fneq1 5979	. . . . . . 7 |- ( `' `' F = F -> ( `' `' F Fn A <-> F Fn A ) )
4	3	biimprd 238	. . . . . 6 |- ( `' `' F = F -> ( F Fn A -> `' `' F Fn A ) )
5	2, 4	sylbi 207	. . . . 5 |- ( Rel F -> ( F Fn A -> `' `' F Fn A ) )
6	1, 5	mpcom 38	. . . 4 |- ( F Fn A -> `' `' F Fn A )
7	6	anim2i 593	. . 3 |- ( ( `' F Fn B /\ F Fn A ) -> ( `' F Fn B /\ `' `' F Fn A ) )
8	7	ancoms 469	. 2 |- ( ( F Fn A /\ `' F Fn B ) -> ( `' F Fn B /\ `' `' F Fn A ) )
9		dff1o4 6145	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
10		dff1o4 6145	. 2 |- ( `' F : B -1-1-onto-> A <-> ( `' F Fn B /\ `' `' F Fn A ) )
11	8, 9, 10	3imtr4i 281	1 |- ( F : A -1-1-onto-> B -> `' F : B -1-1-onto-> A )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   `'ccnv 5113   Rel wrel 5119   Fn wfn 5883   -1-1-onto->wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1ocnvb  6150  f1orescnv  6152  f1imacnv  6153  f1cnv  6160  f1ococnv1  6165  f1oresrab  6395  f1ocnvfv2  6533  f1ocnvdm  6540  f1ocnvfvrneq  6541  fcof1oinvd  6548  fveqf1o  6557  isocnv  6580  weniso  6604  f1ofveu  6645  f1oexrnex  7115  f1oexbi  7116  fnwelem  7292  oacomf1o  7645  mapsnf1o3  7906  ener  8002  enerOLD  8003  en0  8019  en1  8023  omf1o  8063  domss2  8119  mapen  8124  ssenen  8134  f1fi  8253  f1opwfi  8270  mapfienlem2  8311  mapfienlem3  8312  mapfien  8313  mapfien2  8314  ordiso2  8420  unxpwdom2  8493  cantnfle  8568  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cantnflem1  8586  wemapwe  8594  oef1o  8595  cnfcomlem  8596  cnfcom  8597  cnfcom2lem  8598  cnfcom2  8599  cnfcom3lem  8600  cnfcom3  8601  infxpenlem  8836  infxpenc  8841  dfac8b  8854  acndom  8874  acndom2  8877  iunfictbso  8937  dfac12lem2  8966  infpssrlem3  9127  infpssrlem4  9128  fin1a2lem7  9228  axcc3  9260  ttukeylem7  9337  fpwwe2lem6  9457  fpwwe2lem7  9458  pwfseqlem5  9485  axdc4uzlem  12782  seqf1olem1  12840  seqf1olem2  12841  hashfacen  13238  seqcoll  13248  seqcoll2  13249  cnrecnv  13905  isercolllem2  14396  isercoll  14398  summolem3  14445  summolem2a  14446  ackbijnn  14560  prodmolem3  14663  prodmolem2a  14664  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  phimullem  15484  eulerthlem2  15487  unbenlem  15612  1arith2  15632  xpsbas  16234  xpsadd  16236  xpsmul  16237  xpssca  16238  xpsvsca  16239  xpsless  16240  xpsle  16241  setcinv  16740  catcisolem  16756  xpsmnd  17330  mhmf1o  17345  xpsgrp  17534  ghmf1o  17690  symggrp  17820  symginv  17822  f1omvdcnv  17864  f1omvdconj  17866  pmtrfconj  17886  odngen  17992  gsumval3eu  18305  gsumval3  18308  gsumzf1o  18313  lmhmf1o  19046  fidomndrnglem  19306  psrass1lem  19377  coe1sfi  19583  znleval  19903  zntoslem  19905  znunithash  19913  mdetleib2  20394  basqtop  21514  tgqtop  21515  reghmph  21596  indishmph  21601  cmphaushmeo  21603  ordthmeolem  21604  txhmeo  21606  xpstps  21613  xpstopnlem2  21614  qtopf1  21619  ufldom  21766  symgtgp  21905  tgpconncompeqg  21915  xpsdsfn  22182  xpsxmet  22185  xpsdsval  22186  xpsmet  22187  imasf1obl  22293  xpsxms  22339  xpsms  22340  iccpnfcnv  22743  xrhmeo  22745  ovoliunlem2  23271  vitalilem2  23378  mbfimaopnlem  23422  dvcnvlem  23739  dvcnv  23740  dvcnvrelem2  23781  dvcnvre  23782  efif1olem4  24291  eff1olem  24294  logrn  24305  logf1o  24311  dvlog  24397  asinrebnd  24628  sqff1o  24908  lgsqrlem4  25074  cnvmot  25436  f1otrg  25751  f1otrge  25752  cnvunop  28777  unopadj  28778  fresf1o  29433  fmptco1f1o  29434  padct  29497  fcobij  29500  fsumiunle  29575  abliso  29696  madjusmdetlem2  29894  madjusmdetlem4  29896  tpr2rico  29958  esumiun  30156  reprpmtf1o  30704  derangenlem  31153  subfacp1lem4  31165  cvmfolem  31261  cvmliftlem6  31272  fv1stcnv  31680  fv2ndcnv  31681  f1ocan1fv  33521  f1ocan2fv  33522  ismtycnv  33601  ismtyima  33602  ismtyhmeolem  33603  ismtybndlem  33605  rngoisocnv  33780  lautcnv  35376  cdlemk45  36235  cdlemn9  36494  eldioph2  37325  kelac1  37633  brco2f1o  38330  brco3f1o  38331  sge0f1o  40599  mgmhmf1o  41787