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

Theorem frn 5752
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 465 1  |-  ( F : A --> B  ->  ran  F  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3442   ran crn 4855    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 188  df-an 372  df-f 5605
This theorem is referenced by:  fco2  5757  fssxp  5758  fimacnvdisj  5778  f00  5782  f0rn0  5785  foconst  5821  fimacnv  6027  ffvelrn  6035  f1ompt  6059  fnfvrnss  6066  rnmptss  6067  fliftrel  6216  isofr2  6250  fun11iun  6767  f1dmex  6777  fo1stres  6831  fo2ndres  6832  1stcof  6835  2ndcof  6836  fo2ndf  6914  fnwelem  6922  tposf2  7005  onoviun  7070  onnseq  7071  smores2  7081  seqomlem2  7176  oacomf1olem  7273  map0b  7518  mapsn  7521  f1imaen2g  7637  domdifsn  7661  domunsncan  7678  omxpenlem  7679  fodomr  7729  domss2  7737  f1finf1o  7804  f1fi  7867  unirnffid  7872  fissuni  7885  fipreima  7886  indexfi  7888  intrnfi  7936  dffi3  7951  ordtypelem8  8040  ordtypelem9  8041  ordtypelem10  8042  oismo  8055  hartogslem1  8057  brwdom2  8088  unxpwdom2  8103  ixpiunwdom  8106  infdifsn  8161  cantnf  8197  ac10ct  8463  numacn  8478  acndom  8480  acndom2  8483  infpwfien  8491  carduniima  8525  dfac12lem2  8572  dfac12lem3  8573  ackbij1  8666  fictb  8673  cfflb  8687  fin23lem40  8779  fin23lem41  8780  isf34lem5  8806  isf34lem7  8807  isf34lem6  8808  enfin1ai  8812  fin1a2lem6  8833  fin1a2lem7  8834  hsmexlem4  8857  hsmexlem5  8858  axdc2lem  8876  axdc3lem2  8879  ttukeylem6  8942  unirnfdomd  8990  pwcfsdom  9006  smobeth  9009  canthp1lem2  9077  pwfseqlem5  9087  wuncval2  9171  tskurn  9213  wfgru  9240  peano5nni  10612  rpnnen1lem4  11293  rpnnen1lem5  11294  unirnioo  11734  fseqsupcl  12187  fseqsupubi  12188  hashimarn  12605  hashf1lem1  12613  hashf1lem2  12614  ccatrn  12720  swrdrn  12770  cshwrn  12889  limsupcl  13507  limsupclOLD  13508  limsupgle  13513  limsuple  13514  limsupleOLD  13515  limsupval2  13518  limsupval2OLD  13519  limsupgre  13520  limsupgreOLD  13521  isercolllem2  13707  isercoll  13709  isercoll2  13710  climsup  13711  ruclem11  14270  prmreclem6  14828  4sqlem11  14862  vdwapf  14885  vdwlem11  14904  0ram  14941  0ram2  14942  0ramcl  14944  imasdsval2  15373  mrcssv  15471  isacs1i  15514  funcres2b  15753  funcres2c  15757  setcepi  15934  yoniso  16121  isacs4lem  16365  acsmapd  16375  acsmap2d  16376  gsumval1  16471  mhmima  16561  gsumwspan  16581  frmdss2  16598  cycsubgcl  16794  cycsubgss  16795  ghmrn  16847  conjnmz  16867  cntzmhm  16943  f1omvdconj  17038  psgnunilem1  17085  dfod2  17153  odcl2  17154  odf1o2  17160  sylow1lem2  17186  pgpssslw  17201  sylow2blem1  17207  lsmssv  17230  lsmidm  17249  pj1ghm2  17289  efgsp1  17322  efgsfo  17324  efgrelexlemb  17335  cntzcmnf  17418  gexex  17426  iscyggen2  17451  cyggenod  17454  iscyg3  17456  gsumval3eu  17473  gsumval3lem1  17474  gsumval3lem2  17475  gsumval3  17476  gsumzsubmcl  17486  gsumzaddlem  17489  gsumzadd  17490  gsumzsplit  17495  gsumconst  17502  gsumzoppg  17512  gsumpt  17529  dmdprdd  17566  dprdfcntz  17583  dprdfeq0  17590  dprdlub  17594  dprdres  17596  dprdss  17597  dprdz  17598  dprdf1  17601  subgdmdprd  17602  subgdprd  17603  dprd2dlem1  17609  dprd2da  17610  dmdprdsplit2lem  17613  dpjghm2  17632  ablfac1b  17638  lmhmlsp  18207  pj1lmhm2  18259  aspval2  18506  mplcoe5lem  18626  mplbas2  18629  mplind  18660  evlslem1  18673  evlseu  18674  gsumply1subr  18762  pjfo  19209  frlmsplit2  19262  frlmsslsp  19285  frlmlbs  19286  frlmup3  19289  frlmup4  19290  lindff1  19309  lindfrn  19310  f1lindf  19311  lindfmm  19316  indlcim  19329  m2cpmf1  19698  m2cpmghm  19699  m2cpmmhm  19700  iinopn  19863  pptbas  19954  tgrest  20106  resttopon  20108  rest0  20116  restfpw  20126  ordtbaslem  20135  ordtuni  20137  ordtbas2  20138  ordtrest  20149  ordtrest2  20151  leordtval2  20159  lecldbas  20166  cnclsi  20219  cnrest2r  20234  cnprest2  20237  lmss  20245  cncmp  20338  rncmp  20342  discmp  20344  cmpsub  20346  tgcmp  20347  hauscmplem  20352  conima  20371  concn  20372  2ndcctbss  20401  2ndcdisj  20402  2ndcomap  20404  2ndcsep  20405  dis2ndc  20406  lly1stc  20442  comppfsc  20478  kgentop  20488  kgencmp  20491  1stckgenlem  20499  1stckgen  20500  kgencn2  20503  kgencn3  20504  txuni2  20511  ptbasfi  20527  xkoopn  20535  xkouni  20545  txbasval  20552  xkoccn  20565  ptcnplem  20567  upxp  20569  uptx  20571  txtube  20586  txcmplem1  20587  txcmplem2  20588  tx1stc  20596  txkgen  20598  xkoptsub  20600  xkoco1cn  20603  xkoco2cn  20604  xkococnlem  20605  xkococn  20606  xkoinjcn  20633  hmeores  20717  hmphdis  20742  fbasrn  20830  trfilss  20835  trfg  20837  zfbas  20842  uzrest  20843  elfm  20893  imaelfm  20897  rnelfmlem  20898  fclscmpi  20975  alexsublem  20990  alexsubALT  20997  ptcmplem1  20998  ptcmplem3  21000  cnextcn  21013  tmdgsum2  21042  symgtgp  21047  submtmd  21050  subgtgp  21051  subgntr  21052  opnsubg  21053  clsnsg  21055  tgpconcomp  21058  tsmsfbas  21073  tsmsxplem1  21098  prdsdsf  21313  prdsxmetlem  21314  prdsmet  21316  imasdsf1olem  21319  unirnblps  21365  unirnbl  21366  blin2  21375  imasf1oxms  21435  prdsbl  21437  met1stc  21467  met2ndci  21468  prdsxmslem2  21475  tgqioo  21729  xrtgioo  21735  xrge0gsumle  21762  xrge0tsms  21763  metdcn2  21768  metdsf  21776  metdsge  21777  metdscn2  21785  cnmptre  21851  iimulcn  21862  icchmeo  21865  xrhmeo  21870  cnheiborlem  21878  bndth  21882  evth  21883  evth2  21884  lebnumlem2  21886  lebnumlem3  21887  reparphti  21921  tchex  22084  tchnmfval  22095  fmcfil  22135  causs  22161  bcthlem5  22189  minveclem1  22259  minveclem3b  22263  evthicc2  22292  ovolficcss  22301  elovolm  22306  ovolmge0  22308  ovollb  22310  ovolgelb  22311  ovollb2lem  22319  ovollb2  22320  ovolunlem1a  22327  ovolunlem1  22328  ovoliunlem1  22333  ovoliunlem2  22334  ovoliun  22336  ovoliun2  22337  ovolscalem1  22344  ovolicc1  22347  ovolicc2lem4  22351  ovolicc2  22353  voliunlem2  22381  voliunlem3  22382  volsup  22386  ioombl1lem2  22389  ioombl1lem4  22391  uniioovol  22413  uniiccvol  22414  uniioombllem1  22415  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem3  22420  uniioombllem6  22423  uniioombl  22424  dyadmbllem  22434  dyadmbl  22435  opnmbllem  22436  opnmblALT  22438  volsup2  22440  vitalilem2  22444  vitalilem4  22446  vitalilem5  22447  mbfconstlem  22462  mbfsup  22497  mbfinf  22498  mbfinfOLD  22499  mbflimsup  22500  mbflimsupOLD  22501  i1fima  22513  i1fima2  22514  i1fd  22516  itg1cl  22520  itg1ge0  22521  i1f1  22525  itg11  22526  i1fmullem  22529  i1fadd  22530  i1fmul  22531  itg1addlem4  22534  itg1addlem5  22535  i1fmulc  22538  itg1mulc  22539  i1fres  22540  itg10a  22545  itg1ge0a  22546  itg1climres  22549  mbfi1fseqlem4  22553  itg2seq  22577  itg2monolem1  22585  itg2monolem2  22586  itg2monolem3  22587  itg2mono  22588  itg2i1fseq2  22591  itg2gt0  22595  itg2cnlem1  22596  itg2cn  22598  limciun  22726  c1liplem1  22825  dvne0  22840  dvne0f1  22841  lhop2  22844  dvcnvrelem2  22847  dvcnvre  22848  mdegleb  22890  mdeglt  22891  mdegldg  22892  mdegxrcl  22893  mdegcl  22895  ig1peu  22997  aalioulem3  23155  ulmss  23217  reeff1o  23267  efifo  23361  dvlog  23461  efopn  23468  logccv  23473  efrlim  23760  lgamcvg2  23845  basellem3  23872  fsumvma  24004  lgseisenlem4  24143  dchrisum0fno1  24212  edgss  24925  frgrancvvdeqlem8  25613  ghsubgolemOLD  25943  ubthlem1  26357  minvecolem1  26361  htthlem  26405  hhssims  26761  shsss  26801  pjrni  27190  imaelshi  27546  foresf1o  27975  ofrn  28080  ofrn2  28081  fimarab  28084  xppreima2  28089  xrge0tsmsd  28387  smatrcl  28461  locfinreflem  28506  cmpcref  28516  ordtrestNEW  28566  ordtrest2NEW  28568  xrge0mulc1cn  28586  rge0scvg  28594  esumcst  28723  esumpfinvallem  28734  esumpcvgval  28738  esumcvg  28746  esumiun  28754  omssubadd  28961  carsggect  28979  sibfinima  29000  sitgclg  29003  sitgclbn  29004  sitgaddlemb  29009  eulerpartgbij  29031  eulerpartlemgvv  29035  eulerpartlemgf  29038  rrvrnss  29106  orvcval4  29119  ballotlemsima  29174  erdsze2lem2  29715  cvxpcon  29753  cvxscon  29754  cvmsss2  29785  cvmliftlem8  29803  cvmlift3lem6  29835  mrsubrn  29939  mrsubf  29943  msubrn  29955  msubf  29958  mstapst  29973  mvtss  29979  mclsssvlem  29988  mclsax  29995  mclsind  29996  mclsppslem  30009  ghomgrpilem2  30092  ghomfo  30097  orderseqlem  30277  norn  30325  neibastop2lem  30801  tailfb  30818  icoreunrn  31496  ptrecube  31644  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem11  31655  poimirlem12  31656  poimirlem16  31660  poimirlem19  31663  poimirlem27  31671  poimirlem30  31674  poimirlem32  31676  broucube  31678  heicant  31679  opnmbllem0  31680  mblfinlem1  31681  mblfinlem2  31682  mblfinlem3  31683  mblfinlem4  31684  ismblfin  31685  volsupnfl  31689  itg2addnclem2  31698  itg2gt0cn  31701  ftc1anclem3  31723  ftc1anclem5  31725  ftc1anclem6  31726  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  indexdom  31765  cnresima  31800  istotbnd3  31807  sstotbnd2  31810  sstotbnd  31811  totbndbnd  31825  prdsbnd  31829  cntotbnd  31832  ismtyima  31839  heibor1lem  31845  heiborlem1  31847  heibor  31857  rrnval  31863  rrnequiv  31871  reheibor  31875  lsatset  32265  lsatlss  32271  cdleme50rnlem  33820  elrfirn  35246  cmpfiiin  35248  isnacs2  35257  isnacs3  35261  nacsfix  35263  coeq0i  35304  diophrw  35310  eldioph2lem2  35312  dnwech  35612  fnwe2lem2  35615  lmhmfgima  35648  pwssplit4  35653  hbt  35695  imo72b2lem0  36245  imo72b2lem2  36247  imo72b2lem1  36251  imo72b2  36256  refsumcn  36991  cncmpmax  36993  fimass  37065  climinf  37256  climinfOLD  37257  icccncfext  37337  dvsinax  37355  itgsubsticclem  37421  fourierdlem12  37550  fourierdlem42  37580  fourierdlem54  37592  fourierdlem70  37608  fourierdlem76  37614  fourierdlem82  37620  fourierdlem85  37623  fourierdlem88  37626  fourierdlem93  37631  fourierdlem113  37651  fge0npnf  37743  sge0resrnlem  37779  meadjiunlem  37812  omeiunle  37847  fafvelrn  38062  pfxrn  38324  mgmplusfreseq  38531  mgmhmima  38560  elbigolo1  39129  aacllem  39301
  Copyright terms: Public domain W3C validator