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

Theorem frn 5690
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 5543 . 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 3374   ran crn 4792    Fn wfn 5534   -->wf 5535
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 5543
This theorem is referenced by:  fco2  5695  fssxp  5696  fimacnvdisj  5716  f00  5720  f0rn0  5723  foconst  5759  fimacnv  5966  ffvelrn  5974  f1ompt  5998  fnfvrnss  6005  rnmptss  6006  fliftrel  6155  isofr2  6189  fun11iun  6706  f1dmex  6716  fo1stres  6770  fo2ndres  6771  1stcof  6774  2ndcof  6775  fo2ndf  6853  fnwelem  6861  tposf2  6947  onoviun  7012  onnseq  7013  smores2  7023  seqomlem2  7118  oacomf1olem  7215  map0b  7460  mapsn  7463  f1imaen2g  7579  domdifsn  7603  domunsncan  7620  omxpenlem  7621  fodomr  7671  domss2  7679  f1finf1o  7746  f1fi  7809  unirnffid  7814  fissuni  7827  fipreima  7828  indexfi  7830  intrnfi  7878  dffi3  7893  ordtypelem8  7988  ordtypelem9  7989  ordtypelem10  7990  oismo  8003  hartogslem1  8005  brwdom2  8036  unxpwdom2  8051  ixpiunwdom  8054  infdifsn  8109  cantnf  8145  ac10ct  8411  numacn  8426  acndom  8428  acndom2  8431  infpwfien  8439  carduniima  8473  dfac12lem2  8520  dfac12lem3  8521  ackbij1  8614  fictb  8621  cfflb  8635  fin23lem40  8727  fin23lem41  8728  isf34lem5  8754  isf34lem7  8755  isf34lem6  8756  enfin1ai  8760  fin1a2lem6  8781  fin1a2lem7  8782  hsmexlem4  8805  hsmexlem5  8806  axdc2lem  8824  axdc3lem2  8827  ttukeylem6  8890  unirnfdomd  8938  pwcfsdom  8954  smobeth  8957  canthp1lem2  9024  pwfseqlem5  9034  wuncval2  9118  tskurn  9160  wfgru  9187  peano5nni  10558  rpnnen1lem4  11239  rpnnen1lem5  11240  unirnioo  11680  fseqsupcl  12135  fseqsupubi  12136  hashimarn  12553  hashf1lem1  12561  hashf1lem2  12562  ccatrn  12676  swrdrn  12726  cshwrn  12845  limsupcl  13467  limsupclOLD  13468  limsupgle  13473  limsuple  13474  limsupleOLD  13475  limsupval2  13478  limsupval2OLD  13479  limsupgre  13480  limsupgreOLD  13481  isercolllem2  13667  isercoll  13669  isercoll2  13670  climsup  13671  ruclem11  14230  prmreclem6  14803  4sqlem11  14837  vdwapf  14860  vdwlem11  14879  0ram  14916  0ram2  14917  0ramcl  14919  imasdsval2  15355  imasdsval2OLD  15367  mrcssv  15458  isacs1i  15501  funcres2b  15740  funcres2c  15744  setcepi  15921  yoniso  16108  isacs4lem  16352  acsmapd  16362  acsmap2d  16363  gsumval1  16458  mhmima  16548  gsumwspan  16568  frmdss2  16585  cycsubgcl  16781  cycsubgss  16782  ghmrn  16834  conjnmz  16854  cntzmhm  16930  f1omvdconj  17025  psgnunilem1  17072  dfod2  17153  odcl2  17154  odf1o2  17160  sylow1lem2  17189  pgpssslw  17204  sylow2blem1  17210  lsmssv  17233  lsmidm  17252  pj1ghm2  17292  efgsp1  17325  efgsfo  17327  efgrelexlemb  17338  cntzcmnf  17421  gexex  17429  iscyggen2  17454  cyggenod  17457  iscyg3  17459  gsumval3eu  17476  gsumval3lem1  17477  gsumval3lem2  17478  gsumval3  17479  gsumzsubmcl  17489  gsumzaddlem  17492  gsumzadd  17493  gsumzsplit  17498  gsumconst  17505  gsumzoppg  17515  gsumpt  17532  dmdprdd  17569  dprdfcntz  17586  dprdfeq0  17593  dprdlub  17597  dprdres  17599  dprdss  17600  dprdz  17601  dprdf1  17604  subgdmdprd  17605  subgdprd  17606  dprd2dlem1  17612  dprd2da  17613  dmdprdsplit2lem  17616  dpjghm2  17635  ablfac1b  17641  lmhmlsp  18210  pj1lmhm2  18262  aspval2  18509  mplcoe5lem  18629  mplbas2  18632  mplind  18663  evlslem1  18676  evlseu  18677  gsumply1subr  18765  pjfo  19215  frlmsplit2  19268  frlmsslsp  19291  frlmlbs  19292  frlmup3  19295  frlmup4  19296  lindff1  19315  lindfrn  19316  f1lindf  19317  lindfmm  19322  indlcim  19335  m2cpmf1  19704  m2cpmghm  19705  m2cpmmhm  19706  iinopn  19869  pptbas  19960  tgrest  20112  resttopon  20114  rest0  20122  restfpw  20132  ordtbaslem  20141  ordtuni  20143  ordtbas2  20144  ordtrest  20155  ordtrest2  20157  leordtval2  20165  lecldbas  20172  cnclsi  20225  cnrest2r  20240  cnprest2  20243  lmss  20251  cncmp  20344  rncmp  20348  discmp  20350  cmpsub  20352  tgcmp  20353  hauscmplem  20358  conima  20377  concn  20378  2ndcctbss  20407  2ndcdisj  20408  2ndcomap  20410  2ndcsep  20411  dis2ndc  20412  lly1stc  20448  comppfsc  20484  kgentop  20494  kgencmp  20497  1stckgenlem  20505  1stckgen  20506  kgencn2  20509  kgencn3  20510  txuni2  20517  ptbasfi  20533  xkoopn  20541  xkouni  20551  txbasval  20558  xkoccn  20571  ptcnplem  20573  upxp  20575  uptx  20577  txtube  20592  txcmplem1  20593  txcmplem2  20594  tx1stc  20602  txkgen  20604  xkoptsub  20606  xkoco1cn  20609  xkoco2cn  20610  xkococnlem  20611  xkococn  20612  xkoinjcn  20639  hmeores  20723  hmphdis  20748  fbasrn  20836  trfilss  20841  trfg  20843  zfbas  20848  uzrest  20849  elfm  20899  imaelfm  20903  rnelfmlem  20904  fclscmpi  20981  alexsublem  20996  alexsubALT  21003  ptcmplem1  21004  ptcmplem3  21006  cnextcn  21019  tmdgsum2  21048  symgtgp  21053  submtmd  21056  subgtgp  21057  subgntr  21058  opnsubg  21059  clsnsg  21061  tgpconcomp  21064  tsmsfbas  21079  tsmsxplem1  21104  prdsdsf  21319  prdsxmetlem  21320  prdsmet  21322  imasdsf1olem  21325  unirnblps  21371  unirnbl  21372  blin2  21381  imasf1oxms  21441  prdsbl  21443  met1stc  21473  met2ndci  21474  prdsxmslem2  21481  tgqioo  21755  xrtgioo  21761  xrge0gsumle  21788  xrge0tsms  21789  metdcn2  21794  metdsf  21802  metdsge  21803  metdscn2  21811  metdsfOLD  21817  metdsgeOLD  21818  metdscn2OLD  21826  cnmptre  21892  iimulcn  21903  icchmeo  21906  xrhmeo  21911  cnheiborlem  21919  bndth  21923  evth  21924  evth2  21925  lebnumlem2  21927  lebnumlem3  21928  lebnumlem2OLD  21930  lebnumlem3OLD  21931  reparphti  21965  tchex  22128  tchnmfval  22139  fmcfil  22179  causs  22205  bcthlem5  22233  minveclem1  22303  minveclem3b  22307  minveclem3bOLD  22319  evthicc2  22348  ovolficcss  22359  elovolm  22365  ovolmge0  22367  ovollb  22369  ovolgelb  22370  ovollb2lem  22378  ovollb2  22379  ovolunlem1a  22386  ovolunlem1  22387  ovoliunlem1  22392  ovoliunlem2  22393  ovoliun  22395  ovoliun2  22396  ovolscalem1  22403  ovolicc1  22406  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  ovolicc2  22413  voliunlem2  22441  voliunlem3  22442  volsup  22446  ioombl1lem2  22449  ioombl1lem4  22451  uniioovol  22473  uniiccvol  22474  uniioombllem1  22475  uniioombllem2  22477  uniioombllem2OLD  22478  uniioombllem3  22480  uniioombllem6  22483  uniioombl  22484  dyadmbllem  22494  dyadmbl  22495  opnmbllem  22496  opnmblALT  22498  volsup2  22500  vitalilem2  22504  vitalilem4  22506  vitalilem5  22507  mbfconstlem  22522  mbfsup  22557  mbfinf  22558  mbfinfOLD  22559  mbflimsup  22560  mbflimsupOLD  22561  i1fima  22573  i1fima2  22574  i1fd  22576  itg1cl  22580  itg1ge0  22581  i1f1  22585  itg11  22586  i1fmullem  22589  i1fadd  22590  i1fmul  22591  itg1addlem4  22594  itg1addlem5  22595  i1fmulc  22598  itg1mulc  22599  i1fres  22600  itg10a  22605  itg1ge0a  22606  itg1climres  22609  mbfi1fseqlem4  22613  itg2seq  22637  itg2monolem1  22645  itg2monolem2  22646  itg2monolem3  22647  itg2mono  22648  itg2i1fseq2  22651  itg2gt0  22655  itg2cnlem1  22656  itg2cn  22658  limciun  22786  c1liplem1  22885  dvne0  22900  dvne0f1  22901  lhop2  22904  dvcnvrelem2  22907  dvcnvre  22908  mdegleb  22950  mdeglt  22951  mdegldg  22952  mdegxrcl  22953  mdegcl  22955  ig1peu  23059  ig1peuOLD  23060  aalioulem3  23227  ulmss  23289  reeff1o  23339  efifo  23433  dvlog  23533  efopn  23540  logccv  23545  efrlim  23832  lgamcvg2  23917  basellem3  23946  fsumvma  24078  lgseisenlem4  24217  dchrisum0fno1  24286  edgss  25016  frgrancvvdeqlem8  25705  ghsubgolemOLD  26035  ubthlem1  26449  minvecolem1  26453  htthlem  26507  hhssims  26863  shsss  26903  pjrni  27292  imaelshi  27648  foresf1o  28077  ofrn  28181  ofrn2  28182  fimarab  28185  xppreima2  28190  xrge0tsmsd  28495  smatrcl  28569  locfinreflem  28614  cmpcref  28624  ordtrestNEW  28674  ordtrest2NEW  28676  xrge0mulc1cn  28694  rge0scvg  28702  esumcst  28831  esumpfinvallem  28842  esumpcvgval  28846  esumcvg  28854  esumiun  28862  omssubadd  29075  omssubaddOLD  29079  carsggect  29097  sibfinima  29119  sitgclg  29122  sitgclbn  29123  sitgaddlemb  29128  eulerpartgbij  29152  eulerpartlemgvv  29156  eulerpartlemgf  29159  rrvrnss  29227  orvcval4  29240  ballotlemsima  29295  ballotlemsimaOLD  29333  erdsze2lem2  29874  cvxpcon  29912  cvxscon  29913  cvmsss2  29944  cvmliftlem8  29962  cvmlift3lem6  29994  mrsubrn  30098  mrsubf  30102  msubrn  30114  msubf  30117  mstapst  30132  mvtss  30138  mclsssvlem  30147  mclsax  30154  mclsind  30155  mclsppslem  30168  ghomgrpilem2  30251  ghomfo  30256  orderseqlem  30436  norn  30484  neibastop2lem  30960  tailfb  30977  icoreunrn  31669  ptrecube  31847  poimirlem1  31848  poimirlem2  31849  poimirlem3  31850  poimirlem11  31858  poimirlem12  31859  poimirlem16  31863  poimirlem19  31866  poimirlem27  31874  poimirlem30  31877  poimirlem32  31879  broucube  31881  heicant  31882  opnmbllem0  31883  mblfinlem1  31884  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  volsupnfl  31892  itg2addnclem2  31901  itg2gt0cn  31904  ftc1anclem3  31926  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  indexdom  31968  cnresima  32003  istotbnd3  32010  sstotbnd2  32013  sstotbnd  32014  totbndbnd  32028  prdsbnd  32032  cntotbnd  32035  ismtyima  32042  heibor1lem  32048  heiborlem1  32050  heibor  32060  rrnval  32066  rrnequiv  32074  reheibor  32078  lsatset  32468  lsatlss  32474  cdleme50rnlem  34023  elrfirn  35449  cmpfiiin  35451  isnacs2  35460  isnacs3  35464  nacsfix  35466  coeq0i  35507  diophrw  35513  eldioph2lem2  35515  dnwech  35819  fnwe2lem2  35822  lmhmfgima  35855  pwssplit4  35860  hbt  35902  imo72b2lem0  36521  imo72b2lem2  36523  imo72b2lem1  36527  imo72b2  36532  refsumcn  37267  cncmpmax  37269  fimass  37346  climinf  37567  climinfOLD  37568  icccncfext  37648  dvsinax  37666  itgsubsticclem  37735  fourierdlem12  37864  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem54  37907  fourierdlem70  37923  fourierdlem76  37929  fourierdlem82  37935  fourierdlem85  37938  fourierdlem88  37941  fourierdlem93  37946  fourierdlem113  37966  fge0npnf  38060  sge0resrnlem  38096  sge0isum  38120  meadjiunlem  38154  omeiunle  38189  hoicvr  38217  fafvelrn  38485  pfxrn  38747  uhgredg  38986  umgredgss  38987  edgupgr  38988  upgredg  38990  edgass  39006  usgruspgrb  39024  upgrres1  39117  mgmplusfreseq  39364  mgmhmima  39393  elbigolo1  39961  aacllem  40133
  Copyright terms: Public domain W3C validator