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

Theorem frn 5758
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frn  |-  ( F : A --> B  ->  ran  F  C_  B )

Proof of Theorem frn
StepHypRef Expression
1 df-f 5605 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 470 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3416   ran crn 4854    Fn wfn 5596   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 377  df-f 5605
This theorem is referenced by:  fco2  5763  fssxp  5764  fimacnvdisj  5784  f00  5788  f0rn0  5791  foconst  5827  fimacnv  6035  ffvelrn  6043  f1ompt  6067  fnfvrnss  6074  rnmptss  6076  fliftrel  6226  isofr2  6260  fun11iun  6780  f1dmex  6790  fo1stres  6844  fo2ndres  6845  1stcof  6848  2ndcof  6849  fo2ndf  6930  fnwelem  6938  tposf2  7023  onoviun  7088  onnseq  7089  smores2  7099  seqomlem2  7194  oacomf1olem  7291  map0b  7536  mapsn  7539  f1imaen2g  7656  domdifsn  7681  domunsncan  7698  omxpenlem  7699  fodomr  7749  domss2  7757  f1finf1o  7824  f1fi  7887  unirnffid  7892  fissuni  7905  fipreima  7906  indexfi  7908  intrnfi  7956  dffi3  7971  ordtypelem8  8066  ordtypelem9  8067  ordtypelem10  8068  oismo  8081  hartogslem1  8083  brwdom2  8114  unxpwdom2  8129  ixpiunwdom  8132  infdifsn  8188  cantnf  8224  ac10ct  8491  numacn  8506  acndom  8508  acndom2  8511  infpwfien  8519  carduniima  8553  dfac12lem2  8600  dfac12lem3  8601  ackbij1  8694  fictb  8701  cfflb  8715  fin23lem40  8807  fin23lem41  8808  isf34lem5  8834  isf34lem7  8835  isf34lem6  8836  enfin1ai  8840  fin1a2lem6  8861  fin1a2lem7  8862  hsmexlem4  8885  hsmexlem5  8886  axdc2lem  8904  axdc3lem2  8907  ttukeylem6  8970  unirnfdomd  9018  pwcfsdom  9034  smobeth  9037  canthp1lem2  9104  pwfseqlem5  9114  wuncval2  9198  tskurn  9240  wfgru  9267  peano5nni  10640  rpnnen1lem4  11322  rpnnen1lem5  11323  unirnioo  11763  fseqsupcl  12222  fseqsupubi  12223  hashimarn  12643  hashf1lem1  12651  hashf1lem2  12652  ccatrn  12769  swrdrn  12822  cshwrn  12941  limsupcl  13578  limsupclOLD  13579  limsupgle  13584  limsuple  13585  limsupleOLD  13586  limsupval2  13589  limsupval2OLD  13590  limsupgre  13591  limsupgreOLD  13592  isercolllem2  13778  isercoll  13780  isercoll2  13781  climsup  13782  ruclem11  14341  prmreclem6  14914  4sqlem11  14948  vdwapf  14971  vdwlem11  14990  0ram  15027  0ram2  15028  0ramcl  15030  imasdsval2  15466  imasdsval2OLD  15478  mrcssv  15569  isacs1i  15612  funcres2b  15851  funcres2c  15855  setcepi  16032  yoniso  16219  isacs4lem  16463  acsmapd  16473  acsmap2d  16474  gsumval1  16569  mhmima  16659  gsumwspan  16679  frmdss2  16696  cycsubgcl  16892  cycsubgss  16893  ghmrn  16945  conjnmz  16965  cntzmhm  17041  f1omvdconj  17136  psgnunilem1  17183  dfod2  17264  odcl2  17265  odf1o2  17271  sylow1lem2  17300  pgpssslw  17315  sylow2blem1  17321  lsmssv  17344  lsmidm  17363  pj1ghm2  17403  efgsp1  17436  efgsfo  17438  efgrelexlemb  17449  cntzcmnf  17532  gexex  17540  iscyggen2  17565  cyggenod  17568  iscyg3  17570  gsumval3eu  17587  gsumval3lem1  17588  gsumval3lem2  17589  gsumval3  17590  gsumzsubmcl  17600  gsumzaddlem  17603  gsumzadd  17604  gsumzsplit  17609  gsumconst  17616  gsumzoppg  17626  gsumpt  17643  dmdprdd  17680  dprdfcntz  17697  dprdfeq0  17704  dprdlub  17708  dprdres  17710  dprdss  17711  dprdz  17712  dprdf1  17715  subgdmdprd  17716  subgdprd  17717  dprd2dlem1  17723  dprd2da  17724  dmdprdsplit2lem  17727  dpjghm2  17746  ablfac1b  17752  lmhmlsp  18321  pj1lmhm2  18373  aspval2  18620  mplcoe5lem  18740  mplbas2  18743  mplind  18774  evlslem1  18787  evlseu  18788  gsumply1subr  18876  pjfo  19327  frlmsplit2  19380  frlmsslsp  19403  frlmlbs  19404  frlmup3  19407  frlmup4  19408  lindff1  19427  lindfrn  19428  f1lindf  19429  lindfmm  19434  indlcim  19447  m2cpmf1  19816  m2cpmghm  19817  m2cpmmhm  19818  iinopn  19981  pptbas  20072  tgrest  20224  resttopon  20226  rest0  20234  restfpw  20244  ordtbaslem  20253  ordtuni  20255  ordtbas2  20256  ordtrest  20267  ordtrest2  20269  leordtval2  20277  lecldbas  20284  cnclsi  20337  cnrest2r  20352  cnprest2  20355  lmss  20363  cncmp  20456  rncmp  20460  discmp  20462  cmpsub  20464  tgcmp  20465  hauscmplem  20470  conima  20489  concn  20490  2ndcctbss  20519  2ndcdisj  20520  2ndcomap  20522  2ndcsep  20523  dis2ndc  20524  lly1stc  20560  comppfsc  20596  kgentop  20606  kgencmp  20609  1stckgenlem  20617  1stckgen  20618  kgencn2  20621  kgencn3  20622  txuni2  20629  ptbasfi  20645  xkoopn  20653  xkouni  20663  txbasval  20670  xkoccn  20683  ptcnplem  20685  upxp  20687  uptx  20689  txtube  20704  txcmplem1  20705  txcmplem2  20706  tx1stc  20714  txkgen  20716  xkoptsub  20718  xkoco1cn  20721  xkoco2cn  20722  xkococnlem  20723  xkococn  20724  xkoinjcn  20751  hmeores  20835  hmphdis  20860  fbasrn  20948  trfilss  20953  trfg  20955  zfbas  20960  uzrest  20961  elfm  21011  imaelfm  21015  rnelfmlem  21016  fclscmpi  21093  alexsublem  21108  alexsubALT  21115  ptcmplem1  21116  ptcmplem3  21118  cnextcn  21131  tmdgsum2  21160  symgtgp  21165  submtmd  21168  subgtgp  21169  subgntr  21170  opnsubg  21171  clsnsg  21173  tgpconcomp  21176  tsmsfbas  21191  tsmsxplem1  21216  prdsdsf  21431  prdsxmetlem  21432  prdsmet  21434  imasdsf1olem  21437  unirnblps  21483  unirnbl  21484  blin2  21493  imasf1oxms  21553  prdsbl  21555  met1stc  21585  met2ndci  21586  prdsxmslem2  21593  tgqioo  21867  xrtgioo  21873  xrge0gsumle  21900  xrge0tsms  21901  metdcn2  21906  metdsf  21914  metdsge  21915  metdscn2  21923  metdsfOLD  21929  metdsgeOLD  21930  metdscn2OLD  21938  cnmptre  22004  iimulcn  22015  icchmeo  22018  xrhmeo  22023  cnheiborlem  22031  bndth  22035  evth  22036  evth2  22037  lebnumlem2  22039  lebnumlem3  22040  lebnumlem2OLD  22042  lebnumlem3OLD  22043  reparphti  22077  tchex  22240  tchnmfval  22251  fmcfil  22291  causs  22317  bcthlem5  22345  minveclem1  22415  minveclem3b  22419  minveclem3bOLD  22431  evthicc2  22460  ovolficcss  22471  elovolm  22477  ovolmge0  22479  ovollb  22481  ovolgelb  22482  ovollb2lem  22490  ovollb2  22491  ovolunlem1a  22498  ovolunlem1  22499  ovoliunlem1  22504  ovoliunlem2  22505  ovoliun  22507  ovoliun2  22508  ovolscalem1  22515  ovolicc1  22518  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ovolicc2  22525  voliunlem2  22553  voliunlem3  22554  volsup  22558  ioombl1lem2  22561  ioombl1lem4  22563  uniioovol  22585  uniiccvol  22586  uniioombllem1  22587  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem3  22592  uniioombllem6  22595  uniioombl  22596  dyadmbllem  22606  dyadmbl  22607  opnmbllem  22608  opnmblALT  22610  volsup2  22612  vitalilem2  22616  vitalilem4  22618  vitalilem5  22619  mbfconstlem  22634  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  mbflimsup  22672  mbflimsupOLD  22673  i1fima  22685  i1fima2  22686  i1fd  22688  itg1cl  22692  itg1ge0  22693  i1f1  22697  itg11  22698  i1fmullem  22701  i1fadd  22702  i1fmul  22703  itg1addlem4  22706  itg1addlem5  22707  i1fmulc  22710  itg1mulc  22711  i1fres  22712  itg10a  22717  itg1ge0a  22718  itg1climres  22721  mbfi1fseqlem4  22725  itg2seq  22749  itg2monolem1  22757  itg2monolem2  22758  itg2monolem3  22759  itg2mono  22760  itg2i1fseq2  22763  itg2gt0  22767  itg2cnlem1  22768  itg2cn  22770  limciun  22898  c1liplem1  22997  dvne0  23012  dvne0f1  23013  lhop2  23016  dvcnvrelem2  23019  dvcnvre  23020  mdegleb  23062  mdeglt  23063  mdegldg  23064  mdegxrcl  23065  mdegcl  23067  ig1peu  23171  ig1peuOLD  23172  aalioulem3  23339  ulmss  23401  reeff1o  23451  efifo  23545  dvlog  23645  efopn  23652  logccv  23657  efrlim  23944  lgamcvg2  24029  basellem3  24058  fsumvma  24190  lgseisenlem4  24329  dchrisum0fno1  24398  edgss  25128  frgrancvvdeqlem8  25817  ghsubgolemOLD  26147  ubthlem1  26561  minvecolem1  26565  htthlem  26619  hhssims  26975  shsss  27015  pjrni  27404  imaelshi  27760  foresf1o  28188  ofrn  28289  ofrn2  28290  fimarab  28293  xppreima2  28298  xrge0tsmsd  28597  smatrcl  28671  locfinreflem  28716  cmpcref  28726  ordtrestNEW  28776  ordtrest2NEW  28778  xrge0mulc1cn  28796  rge0scvg  28804  esumcst  28933  esumpfinvallem  28944  esumpcvgval  28948  esumcvg  28956  esumiun  28964  omssubadd  29177  omssubaddOLD  29181  carsggect  29199  sibfinima  29221  sitgclg  29224  sitgclbn  29225  sitgaddlemb  29230  eulerpartgbij  29254  eulerpartlemgvv  29258  eulerpartlemgf  29261  rrvrnss  29329  orvcval4  29342  ballotlemsima  29397  ballotlemsimaOLD  29435  erdsze2lem2  29976  cvxpcon  30014  cvxscon  30015  cvmsss2  30046  cvmliftlem8  30064  cvmlift3lem6  30096  mrsubrn  30200  mrsubf  30204  msubrn  30216  msubf  30219  mstapst  30234  mvtss  30240  mclsssvlem  30249  mclsax  30256  mclsind  30257  mclsppslem  30270  ghomgrpilem2  30353  ghomfo  30358  orderseqlem  30539  norn  30587  neibastop2lem  31065  tailfb  31082  icoreunrn  31807  ptrecube  31985  poimirlem1  31986  poimirlem2  31987  poimirlem3  31988  poimirlem11  31996  poimirlem12  31997  poimirlem16  32001  poimirlem19  32004  poimirlem27  32012  poimirlem30  32015  poimirlem32  32017  broucube  32019  heicant  32020  opnmbllem0  32021  mblfinlem1  32022  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  volsupnfl  32030  itg2addnclem2  32039  itg2gt0cn  32042  ftc1anclem3  32064  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  indexdom  32106  cnresima  32141  istotbnd3  32148  sstotbnd2  32151  sstotbnd  32152  totbndbnd  32166  prdsbnd  32170  cntotbnd  32173  ismtyima  32180  heibor1lem  32186  heiborlem1  32188  heibor  32198  rrnval  32204  rrnequiv  32212  reheibor  32216  lsatset  32601  lsatlss  32607  cdleme50rnlem  34156  elrfirn  35582  cmpfiiin  35584  isnacs2  35593  isnacs3  35597  nacsfix  35599  coeq0i  35640  diophrw  35646  eldioph2lem2  35648  dnwech  35951  fnwe2lem2  35954  lmhmfgima  35987  pwssplit4  35992  hbt  36034  imo72b2lem0  36653  imo72b2lem2  36655  imo72b2lem1  36659  imo72b2  36663  refsumcn  37391  cncmpmax  37393  fimass  37481  mapsnd  37514  climinf  37722  climinfOLD  37723  icccncfext  37803  dvsinax  37821  itgsubsticclem  37890  fourierdlem12  38019  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem54  38062  fourierdlem70  38078  fourierdlem76  38084  fourierdlem82  38090  fourierdlem85  38093  fourierdlem88  38096  fourierdlem93  38101  fourierdlem113  38121  fge0npnf  38247  sge0resrnlem  38283  sge0isum  38307  meadjiunlem  38341  omeiunle  38376  hoicvr  38408  fafvelrn  38710  pfxrn  38974  uhgredgn0  39268  upgredgss  39271  umgredgss  39272  edgupgr  39273  upgredg  39276  usgredgss  39295  usgruspgrb  39316  upgrres1  39430  mgmplusfreseq  40046  mgmhmima  40075  elbigolo1  40641  aacllem  40813
  Copyright terms: Public domain W3C validator