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

Theorem f1ocnv 6797
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 6605 . . . 4 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel2 6142 . . . . 5 (Rel 𝐹𝐹 = 𝐹)
3 fneq1 6594 . . . . . 6 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
43biimprd 248 . . . . 5 (𝐹 = 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
52, 4sylbi 216 . . . 4 (Rel 𝐹 → (𝐹 Fn 𝐴𝐹 Fn 𝐴))
61, 5mpcom 38 . . 3 (𝐹 Fn 𝐴𝐹 Fn 𝐴)
76anim1ci 617 . 2 ((𝐹 Fn 𝐴𝐹 Fn 𝐵) → (𝐹 Fn 𝐵𝐹 Fn 𝐴))
8 dff1o4 6793 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴𝐹 Fn 𝐵))
9 dff1o4 6793 . 2 (𝐹:𝐵1-1-onto𝐴 ↔ (𝐹 Fn 𝐵𝐹 Fn 𝐴))
107, 8, 93imtr4i 292 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐵1-1-onto𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  ccnv 5633  Rel wrel 5639   Fn wfn 6492  1-1-ontowf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  f1ocnvb  6798  f1orescnv  6800  f1imacnv  6801  f1cnv  6809  f1ococnv1  6814  f1oresrab  7074  f1ocnvfv2  7224  f1ocnvdm  7232  f1ocnvfvrneq  7233  fcof1oinvd  7240  fveqf1o  7250  isocnv  7276  weniso  7300  f1ofveu  7352  f1oexrnex  7865  f1oexbi  7866  fnwelem  8064  oacomf1o  8513  mapsnf1o3  8834  ener  8942  en0  8958  en0OLD  8959  en0ALT  8960  en1  8966  en1OLD  8967  omf1o  9020  domss2  9081  mapen  9086  ssenen  9096  f1oenfirn  9128  ensymfib  9132  snnen2o  9182  1sdom2dom  9192  infn0  9252  f1fi  9284  f1opwfi  9301  mapfienlem2  9343  mapfienlem3  9344  mapfien  9345  mapfien2  9346  ordiso2  9452  unxpwdom2  9525  cantnfle  9608  cantnfp1lem3  9617  cantnflem1b  9623  cantnflem1d  9625  cantnflem1  9626  wemapwe  9634  oef1o  9635  cnfcomlem  9636  cnfcom  9637  cnfcom2lem  9638  cnfcom2  9639  cnfcom3lem  9640  cnfcom3  9641  infxpenlem  9950  infxpenc  9955  dfac8b  9968  acndom  9988  acndom2  9991  iunfictbso  10051  dfac12lem2  10081  infpssrlem3  10242  infpssrlem4  10243  fin1a2lem7  10343  axcc3  10375  ttukeylem7  10452  fpwwe2lem5  10572  fpwwe2lem6  10573  pwfseqlem5  10600  axdc4uzlem  13889  seqf1olem1  13948  seqf1olem2  13949  hashfacen  14352  hashfacenOLD  14353  seqcoll  14364  seqcoll2  14365  cnrecnv  15051  isercolllem2  15551  isercoll  15553  summolem3  15600  summolem2a  15601  ackbijnn  15714  prodmolem3  15817  prodmolem2a  15818  sadcaddlem  16338  sadadd2lem  16340  sadadd3  16342  sadaddlem  16347  sadasslem  16351  sadeq  16353  phimullem  16652  eulerthlem2  16655  unbenlem  16781  1arith2  16801  xpsbas  17455  xpsadd  17457  xpsmul  17458  xpssca  17459  xpsvsca  17460  xpsless  17461  xpsle  17462  setcinv  17977  catcisolem  17997  xpsmnd  18597  mhmf1o  18613  xpsgrp  18867  ghmf1o  19039  symggrp  19183  symginv  19185  f1omvdcnv  19227  f1omvdconj  19229  pmtrfconj  19249  odngen  19360  gsumval3eu  19682  gsumval3  19685  gsumzf1o  19690  lmhmf1o  20510  fidomndrnglem  20780  znleval  20964  zntoslem  20966  znunithash  20974  psrass1lemOLD  21345  psrass1lem  21348  coe1sfi  21587  mdetleib2  21940  basqtop  23065  tgqtop  23066  reghmph  23147  indishmph  23152  cmphaushmeo  23154  ordthmeolem  23155  txhmeo  23157  xpstps  23164  xpstopnlem2  23165  qtopf1  23170  ufldom  23316  symgtgp  23460  tgpconncompeqg  23466  xpsdsfn  23733  xpsxmet  23736  xpsdsval  23737  xpsmet  23738  imasf1obl  23847  xpsxms  23893  xpsms  23894  iccpnfcnv  24310  xrhmeo  24312  ovoliunlem2  24870  vitalilem2  24976  mbfimaopnlem  25022  dvcnvlem  25343  dvcnv  25344  dvcnvrelem2  25385  dvcnvre  25386  efif1olem4  25904  eff1olem  25907  logrn  25917  logf1o  25923  dvlog  26009  asinrebnd  26254  sqff1o  26534  lgsqrlem4  26700  cnvmot  27486  f1otrg  27816  f1otrge  27817  cnvunop  30863  unopadj  30864  fresf1o  31548  fmptco1f1o  31550  padct  31639  fcobij  31642  fsumiunle  31728  abliso  31890  symgcom  31937  tocycfvres1  31962  tocycfvres2  31963  cycpmcl  31968  cycpmconjvlem  31993  cycpmconjv  31994  cycpmconjslem1  32006  cycpmconjslem2  32007  cycpmconjs  32008  madjusmdetlem2  32412  madjusmdetlem4  32414  tpr2rico  32496  esumiun  32696  reprpmtf1o  33242  derangenlem  33768  subfacp1lem4  33780  cvmfolem  33876  cvmliftlem6  33887  fv1stcnv  34354  fv2ndcnv  34355  f1ocan1fv  36188  f1ocan2fv  36189  ismtycnv  36264  ismtyima  36265  ismtyhmeolem  36266  ismtybndlem  36268  rngoisocnv  36443  lautcnv  38556  cdlemk45  39413  cdlemn9  39671  sticksstones18  40575  sticksstones19  40576  metakunt34  40613  eldioph2  41088  kelac1  41393  brco2f1o  42311  brco3f1o  42312  sge0f1o  44630  isomushgr  46025  isomgrsym  46035  mgmhmf1o  46088
  Copyright terms: Public domain W3C validator