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

Theorem frn 5560
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 5417 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
21simprbi 464 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3323   ran crn 4836    Fn wfn 5408   -->wf 5409
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 185  df-an 371  df-f 5417
This theorem is referenced by:  fco2  5564  fssxp  5565  fimacnvdisj  5584  f00  5588  foconst  5626  fimacnv  5830  ffvelrn  5836  f1ompt  5860  fnfvrnss  5866  rnmptss  5867  fliftrel  5996  isofr2  6030  fun11iun  6532  f1dmex  6542  fo1stres  6595  fo2ndres  6596  1stcof  6599  2ndcof  6600  fo2ndf  6674  fnwelem  6682  tposf2  6764  iunon  6791  iinon  6793  onoviun  6796  onnseq  6797  smores2  6807  seqomlem2  6898  oacomf1olem  6995  map0b  7243  mapsn  7246  f1imaen2g  7362  domdifsn  7386  domunsncan  7403  omxpenlem  7404  fodomr  7454  domss2  7462  f1finf1o  7531  f1fi  7590  unirnffid  7595  fissuni  7608  fipreima  7609  indexfi  7611  intrnfi  7658  dffi3  7673  ordtypelem8  7731  ordtypelem9  7732  ordtypelem10  7733  oismo  7746  hartogslem1  7748  brwdom2  7780  unxpwdom2  7795  ixpiunwdom  7798  infdifsn  7854  cantnf  7893  cantnfOLD  7915  ac10ct  8196  numacn  8211  acndom  8213  acndom2  8216  infpwfien  8224  carduniima  8258  dfac12lem2  8305  dfac12lem3  8306  ackbij1  8399  fictb  8406  cfflb  8420  fin23lem40  8512  fin23lem41  8513  isf34lem5  8539  isf34lem7  8540  isf34lem6  8541  enfin1ai  8545  fin1a2lem6  8566  fin1a2lem7  8567  hsmexlem4  8590  hsmexlem5  8591  axdc2lem  8609  axdc3lem2  8612  ttukeylem6  8675  unirnfdomd  8723  pwcfsdom  8739  smobeth  8742  canthp1lem2  8812  pwfseqlem5  8822  wuncval2  8906  tskurn  8948  wfgru  8975  peano5nni  10317  rpnnen1lem4  10974  rpnnen1lem5  10975  unirnioo  11381  fseqsupcl  11791  fseqsupubi  11792  hashimarn  12192  hashf1lem1  12200  hashf1lem2  12201  swrdrn  12315  cshwrn  12431  limsupcl  12943  limsupgle  12947  limsuple  12948  limsupval2  12950  limsupgre  12951  isercolllem2  13135  isercoll  13137  isercoll2  13138  climsup  13139  ruclem11  13514  prmreclem6  13974  4sqlem11  14008  vdwapf  14025  vdwlem11  14044  0ram  14073  0ram2  14074  0ramcl  14076  imasdsval2  14446  mrcssv  14544  isacs1i  14587  funcres2b  14799  funcres2c  14803  setcepi  14948  yoniso  15087  isacs4lem  15330  acsmapd  15340  acsmap2d  15341  mhmima  15482  gsumval1  15500  gsumwspan  15515  frmdss2  15532  cycsubgcl  15698  cycsubgss  15699  ghmrn  15751  conjnmz  15771  cntzmhm  15847  f1omvdconj  15943  psgnunilem1  15990  dfod2  16056  odcl2  16057  odf1o2  16063  sylow1lem2  16089  pgpssslw  16104  sylow2blem1  16110  lsmssv  16133  lsmidm  16152  pj1ghm2  16192  efgsp1  16225  efgsfo  16227  efgrelexlemb  16238  cntzcmnf  16318  gexex  16326  iscyggen2  16349  cyggenod  16352  iscyg3  16354  gsumval3eu  16372  gsumval3OLD  16373  gsumval3lem1  16374  gsumval3lem2  16375  gsumval3  16376  gsumzsubmcl  16393  gsumzsubmclOLD  16394  gsumzaddlem  16399  gsumzadd  16400  gsumzaddlemOLD  16401  gsumzaddOLD  16402  gsumzsplit  16409  gsumzsplitOLD  16410  gsumconst  16417  gsumzoppg  16430  gsumzoppgOLD  16431  gsumpt  16444  gsumptOLD  16445  dmdprdd  16471  dprdfcntz  16489  dprdfcntzOLD  16495  dprdfeq0  16502  dprdfeq0OLD  16509  dprdlub  16513  dprdres  16515  dprdss  16516  dprdz  16517  dprdf1  16520  subgdmdprd  16521  subgdprd  16522  dprd2dlem1  16530  dprd2da  16531  dmdprdsplit2lem  16534  dpjghm2  16553  ablfac1b  16561  lmhmlsp  17110  pj1lmhm2  17162  aspval2  17397  mplcoe5lem  17527  mplbas2  17531  mplbas2OLD  17532  mplind  17564  evlslem1  17581  evlseu  17582  gsumply1subr  17668  pjfo  18120  frlmsplit2  18177  frlmsslsp  18203  frlmsslspOLD  18204  frlmlbs  18205  frlmup3  18208  frlmup4  18209  lindff1  18229  lindfrn  18230  f1lindf  18231  lindfmm  18236  indlcim  18249  iinopn  18495  tgiun  18564  pptbas  18592  tgrest  18743  resttopon  18745  rest0  18753  restfpw  18763  ordtbaslem  18772  ordtuni  18774  ordtbas2  18775  ordtrest  18786  ordtrest2  18788  leordtval2  18796  lecldbas  18803  cnclsi  18856  cnrest  18869  cnrest2r  18871  cnprest2  18874  lmss  18882  cncmp  18975  rncmp  18979  discmp  18981  cmpsub  18983  tgcmp  18984  hauscmplem  18989  bwthOLD  18994  conima  19009  concn  19010  2ndcctbss  19039  2ndcdisj  19040  2ndcomap  19042  2ndcsep  19043  dis2ndc  19044  lly1stc  19080  kgentop  19095  kgencmp  19098  1stckgenlem  19106  1stckgen  19107  kgencn2  19110  kgencn3  19111  txuni2  19118  ptbasfi  19134  xkoopn  19142  xkouni  19152  txbasval  19159  xkoccn  19172  ptcnplem  19174  upxp  19176  uptx  19178  txtube  19193  txcmplem1  19194  txcmplem2  19195  tx1stc  19203  txkgen  19205  xkoptsub  19207  xkoco1cn  19210  xkoco2cn  19211  xkococnlem  19212  xkococn  19213  xkoinjcn  19240  hmeores  19324  hmphdis  19349  fbasrn  19437  trfilss  19442  trfg  19444  zfbas  19449  uzrest  19450  elfm  19500  imaelfm  19504  rnelfmlem  19505  fclscmpi  19582  alexsublem  19596  alexsubALT  19603  ptcmplem1  19604  ptcmplem3  19606  cnextcn  19619  tmdgsum2  19647  symgtgp  19652  submtmd  19655  subgtgp  19656  subgntr  19657  opnsubg  19658  clsnsg  19660  tgpconcomp  19663  tsmsfbas  19678  tsmsxplem1  19707  prdsdsf  19922  prdsxmetlem  19923  prdsmet  19925  imasdsf1olem  19928  unirnblps  19974  unirnbl  19975  blin2  19984  imasf1oxms  20044  prdsbl  20046  met1stc  20076  met2ndci  20077  prdsxmslem2  20084  tgqioo  20357  xrtgioo  20363  xrge0gsumle  20390  xrge0tsms  20391  metdcn2  20396  metdsf  20404  metdsge  20405  metdscn2  20413  cnmptre  20479  iimulcn  20490  icchmeo  20493  xrhmeo  20498  cnheiborlem  20506  bndth  20510  evth  20511  evth2  20512  lebnumlem2  20514  lebnumlem3  20515  reparphti  20549  tchex  20712  tchnmfval  20723  fmcfil  20763  causs  20789  bcthlem5  20819  minveclem1  20891  minveclem3b  20895  evthicc2  20924  ovolficcss  20933  elovolm  20938  ovolmge0  20940  ovollb  20942  ovolgelb  20943  ovollb2lem  20951  ovollb2  20952  ovolunlem1a  20959  ovolunlem1  20960  ovoliunlem1  20965  ovoliunlem2  20966  ovoliun  20968  ovoliun2  20969  ovolscalem1  20976  ovolicc1  20979  ovolicc2lem4  20983  ovolicc2  20985  voliunlem2  21012  voliunlem3  21013  volsup  21017  ioombl1lem2  21020  ioombl1lem4  21022  uniioovol  21039  uniiccvol  21040  uniioombllem1  21041  uniioombllem2  21043  uniioombllem3  21045  uniioombllem6  21048  uniioombl  21049  dyadmbllem  21059  dyadmbl  21060  opnmbllem  21061  opnmblALT  21063  volsup2  21065  vitalilem2  21069  vitalilem4  21071  vitalilem5  21072  mbfconstlem  21087  mbfsup  21122  mbfinf  21123  mbflimsup  21124  i1fima  21136  i1fima2  21137  i1fd  21139  itg1cl  21143  itg1ge0  21144  i1f1  21148  itg11  21149  i1fmullem  21152  i1fadd  21153  i1fmul  21154  itg1addlem4  21157  itg1addlem5  21158  i1fmulc  21161  itg1mulc  21162  i1fres  21163  itg10a  21168  itg1ge0a  21169  itg1climres  21172  mbfi1fseqlem4  21176  itg2seq  21200  itg2monolem1  21208  itg2monolem2  21209  itg2monolem3  21210  itg2mono  21211  itg2i1fseq2  21214  itg2gt0  21218  itg2cnlem1  21219  itg2cn  21221  limciun  21349  c1liplem1  21448  dvne0  21463  dvne0f1  21464  lhop2  21467  dvcnvrelem2  21470  dvcnvre  21471  mdegleb  21515  mdeglt  21516  mdegldg  21517  mdegxrcl  21518  mdegcl  21520  ig1peu  21623  aalioulem3  21780  ulmss  21842  reeff1o  21892  efifo  21983  dvlog  22076  efopn  22083  logccv  22088  efrlim  22343  basellem3  22400  fsumvma  22532  lgseisenlem4  22671  dchrisum0fno1  22740  ghsubgolem  23825  ubthlem1  24239  minvecolem1  24243  htthlem  24287  hhssims  24644  shsss  24684  pjrni  25073  imaelshi  25430  ofrn  25925  ofrn2  25926  xppreima2  25933  xrge0tsmsd  26221  ordtrestNEW  26320  ordtrest2NEW  26322  xrge0mulc1cn  26340  rge0scvg  26348  esumcst  26483  esumpfinvallem  26492  esumpcvgval  26496  esumcvg  26504  sibfinima  26694  sitgclg  26697  sitgclbn  26698  eulerpartgbij  26724  eulerpartlemgvv  26728  eulerpartlemgf  26731  rrvrnss  26799  orvcval4  26812  ballotlemsima  26867  lgamcvg2  27010  erdsze2lem2  27061  cvxpcon  27100  cvxscon  27101  cvmsss2  27132  cvmliftlem8  27150  cvmlift3lem6  27182  ghomgrpilem2  27274  ghomfo  27279  orderseqlem  27682  norn  27761  heicant  28397  opnmbllem0  28398  mblfinlem1  28399  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  volsupnfl  28407  itg2addnclem2  28415  itg2gt0cn  28418  ftc1anclem3  28440  ftc1anclem5  28442  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  comppfsc  28550  neibastop2lem  28552  tailfb  28569  indexdom  28599  cnresima  28634  istotbnd3  28641  sstotbnd2  28644  sstotbnd  28645  totbndbnd  28659  prdsbnd  28663  cntotbnd  28666  ismtyima  28673  heibor1lem  28679  heiborlem1  28681  heibor  28691  rrnval  28697  rrnequiv  28705  reheibor  28709  elrfirn  29002  cmpfiiin  29004  isnacs2  29013  isnacs3  29017  nacsfix  29019  coeq0i  29062  diophrw  29068  eldioph2lem2  29070  dnwech  29372  fnwe2lem2  29375  lmhmfgima  29408  pwssplit4  29413  hbt  29457  refsumcn  29723  cncmpmax  29725  climinf  29750  fafvelrn  30047  f0rn0  30112  frgrancvvdeqlem8  30604  lsatset  32528  lsatlss  32534  cdleme50rnlem  34081
  Copyright terms: Public domain W3C validator