MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1ocnv Structured version   Visualization version   GIF version

Theorem f1ocnv 6624
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
StepHypRef Expression
1 fnrel 6451 . . . 4 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel2 6044 . . . . 5 (Rel 𝐹𝐹 = 𝐹)
3 fneq1 6441 . . . . . 6 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
43biimprd 249 . . . . 5 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
52, 4sylbi 218 . . . 4 (Rel 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
61, 5mpcom 38 . . 3 (𝐹 Fn 𝐴𝐹 Fn 𝐴)
76anim1ci 615 . 2 ((𝐹 Fn 𝐴𝐹 Fn 𝐵) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
8 dff1o4 6620 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
9 dff1o4 6620 . 2 (𝐹:𝐵1-1-onto𝐴 ↔ (𝐹 Fn 𝐵𝐹 Fn 𝐴))
107, 8, 93imtr4i 293 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  ccnv 5553  Rel wrel 5559   Fn wfn 6347  1-1-ontowf1o 6351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359
This theorem is referenced by:  f1ocnvb  6625  f1orescnv  6627  f1imacnv  6628  f1cnv  6635  f1ococnv1  6640  f1oresrab  6885  f1ocnvfv2  7028  f1ocnvdm  7035  f1ocnvfvrneq  7036  fcof1oinvd  7043  fveqf1o  7052  isocnv  7075  weniso  7099  f1ofveu  7143  f1oexrnex  7620  f1oexbi  7621  fnwelem  7816  oacomf1o  8181  mapsnf1o3  8448  ener  8545  en0  8561  en1  8565  omf1o  8609  domss2  8665  mapen  8670  ssenen  8680  f1fi  8800  f1opwfi  8817  mapfienlem2  8858  mapfienlem3  8859  mapfien  8860  mapfien2  8861  ordiso2  8968  unxpwdom2  9041  cantnfle  9123  cantnfp1lem3  9132  cantnflem1b  9138  cantnflem1d  9140  cantnflem1  9141  wemapwe  9149  oef1o  9150  cnfcomlem  9151  cnfcom  9152  cnfcom2lem  9153  cnfcom2  9154  cnfcom3lem  9155  cnfcom3  9156  infxpenlem  9428  infxpenc  9433  dfac8b  9446  acndom  9466  acndom2  9469  iunfictbso  9529  dfac12lem2  9559  infpssrlem3  9716  infpssrlem4  9717  fin1a2lem7  9817  axcc3  9849  ttukeylem7  9926  fpwwe2lem6  10046  fpwwe2lem7  10047  pwfseqlem5  10074  axdc4uzlem  13341  seqf1olem1  13399  seqf1olem2  13400  hashfacen  13802  seqcoll  13812  seqcoll2  13813  cnrecnv  14514  isercolllem2  15012  isercoll  15014  summolem3  15061  summolem2a  15062  ackbijnn  15173  prodmolem3  15277  prodmolem2a  15278  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadaddlem  15805  sadasslem  15809  sadeq  15811  phimullem  16106  eulerthlem2  16109  unbenlem  16234  1arith2  16254  xpsbas  16835  xpsadd  16837  xpsmul  16838  xpssca  16839  xpsvsca  16840  xpsless  16841  xpsle  16842  setcinv  17340  catcisolem  17356  xpsmnd  17939  mhmf1o  17954  xpsgrp  18148  ghmf1o  18318  symggrp  18448  symginv  18450  f1omvdcnv  18492  f1omvdconj  18494  pmtrfconj  18514  odngen  18622  gsumval3eu  18944  gsumval3  18947  gsumzf1o  18952  lmhmf1o  19738  fidomndrnglem  19998  psrass1lem  20076  coe1sfi  20298  znleval  20617  zntoslem  20619  znunithash  20627  mdetleib2  21113  basqtop  22235  tgqtop  22236  reghmph  22317  indishmph  22322  cmphaushmeo  22324  ordthmeolem  22325  txhmeo  22327  xpstps  22334  xpstopnlem2  22335  qtopf1  22340  ufldom  22486  symgtgp  22625  tgpconncompeqg  22635  xpsdsfn  22902  xpsxmet  22905  xpsdsval  22906  xpsmet  22907  imasf1obl  23013  xpsxms  23059  xpsms  23060  iccpnfcnv  23463  xrhmeo  23465  ovoliunlem2  24019  vitalilem2  24125  mbfimaopnlem  24171  dvcnvlem  24488  dvcnv  24489  dvcnvrelem2  24530  dvcnvre  24531  efif1olem4  25042  eff1olem  25045  logrn  25055  logf1o  25061  dvlog  25147  asinrebnd  25392  sqff1o  25673  lgsqrlem4  25839  cnvmot  26241  f1otrg  26571  f1otrge  26572  cnvunop  29609  unopadj  29610  fresf1o  30291  fmptco1f1o  30293  padct  30368  fcobij  30371  fsumiunle  30459  abliso  30597  symgcom  30641  tocycfvres1  30666  tocycfvres2  30667  cycpmcl  30672  cycpmconjvlem  30697  cycpmconjv  30698  cycpmconjslem1  30710  cycpmconjslem2  30711  cycpmconjs  30712  madjusmdetlem2  30979  madjusmdetlem4  30981  tpr2rico  31041  esumiun  31239  reprpmtf1o  31783  derangenlem  32302  subfacp1lem4  32314  cvmfolem  32410  cvmliftlem6  32421  fv1stcnv  32904  fv2ndcnv  32905  f1ocan1fv  34869  f1ocan2fv  34870  ismtycnv  34948  ismtyima  34949  ismtyhmeolem  34950  ismtybndlem  34952  rngoisocnv  35127  lautcnv  37093  cdlemk45  37950  cdlemn9  38208  eldioph2  39224  kelac1  39528  brco2f1o  40247  brco3f1o  40248  sge0f1o  42530  isomushgr  43823  isomgrsym  43833  mgmhmf1o  43886
  Copyright terms: Public domain W3C validator