Theorem ffvelrn 4787

Description: A function's value belongs to its codomain.

Assertion

Ref	Expression
ffvelrn	|- ((F:A-->B /\ C e. A) -> (F` C) e. B)

Proof of Theorem ffvelrn

Step	Hyp	Ref	Expression
1		fnfvelrn 4786	. . 3 |- ((F Fn A /\ C e. A) -> (F` C) e. ran F)
2		ffn 4562	. . 3 |- (F:A-->B -> F Fn A)
3	1, 2	sylan 497	. 2 |- ((F:A-->B /\ C e. A) -> (F` C) e. ran F)
4		frn 4569	. . . 4 |- (F:A-->B -> ran F C_ B)
5	4	sseld 2619	. . 3 |- (F:A-->B -> ((F` C) e. ran F -> (F` C) e. B))
6	5	adantr 425	. 2 |- ((F:A-->B /\ C e. A) -> ((F` C) e. ran F -> (F` C) e. B))
7	3, 6	mpd 29	1 |- ((F:A-->B /\ C e. A) -> (F` C) e. B)

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  ran crn 3987   Fn wfn 3993  -->wf 3994  ` cfv 3998

This theorem is referenced by:  ffvelrni 4788  dffo3 4792  fopab2 4796  ffnfv 4801  fopabco 4805  fsn2 4809  fvconst 4814  f1ocnvfv3 4859  f1ocnvdm 4860  isocnv 4873  isotr 4874  isotrALT 4875  foprrn 4965  omsmolem 5313  omsmo 5314  2dom 5486  xpdom2 5501  pw2en 5505  mapenlem2 5584  mapxpen 5589  xpmapenlem3 5592  xpmapenlem4 5593  xpmapenlem5 5594  unifi 5648  fiint 5650  ordiso 5683  hartog 5693  unidom 5970  fsequb2 7703  seq1rn2 7734  seq1rn 7735  seq1cl 7738  seq1cl2 7739  ser1recli 7744  seqzrn2 7799  seqzrn 7800  seq1bndi 8162  clm4fi 8342  climfnn 8352  climubii 8413  infcvglem3 8484  cncffvelrnOLD 8529  cncffvelrn 8530  efseq0ex 8573  acdc3lem 8754  acdclem 8763  acdcALT 8765  ruclem13 8791  ruclem15 8793  ruclem22 8800  ruclem23 8801  ruclem24 8802  ruclem25 8803  ruclem26 8804  ruclem27 8805  ruclem28 8806  ruclem29 8807  cnpcl 9040  cnpco 9046  metcnplem 9164  metcnp 9165  metcnp2 9166  metcnpi3 9170  metcnpi4 9171  metcni2 9173  metcnss 9176  cncfmet 9183  lmbrf 9208  lmnn 9213  iscauf 9217  iscau5 9219  iscaunns 9222  lmss 9231  causs 9233  metelcls 9243  metcnp4 9248  xplmi 9251  xpcn 9254  oprcn 9255  bopcnlem2 9260  bopcnlem4 9262  cncms 9276  bcthlem4 9280  bcthlem16 9292  bcthlem17 9293  bcthlem18 9294  bcthlem33 9309  nvcl 9619  nvcni 9661  nvcni2 9662  nvcni3 9663  nvlmle 9665  vacnlem5 9671  vacnlem6 9672  sqcn 9674  lno0 9756  lnoadd 9758  lnosub 9759  lnomul 9760  nvcnpi3 9761  nvcnpi4 9762  nmosetre 9766  nmoge0 9769  nmoub3i 9775  nmounbi 9778  blometi 9803  phoeqi 9859  ubthlem3 9874  ubthlem5 9876  ubthlem11 9882  ubthlem12 9883  ubthlem12OLD 9884  minveclem4 9893  minveclem9 9898  minveclem16 9905  minveclem17 9906  minveclem28 9917  htthlem1 9967  htthlem5 9971  htthlem6 9972  htthlem8 9974  htthlem9 9975  ghomid 10197  upxp 10225  uptx 10226  txcnopab 10228  fbssint 10279  h2hcau 10481  h2hlm 10482  hcau2 10688  hhcms 10705  hhsscms 10783  occllem4 10809  occllem6 10811  occli 10814  projlem21 10839  projlem24 10842  projlem25 10843  projlem26 10844  hoscl 11156  homcl 11157  hodcl 11158  osumlem4 11216  osumlem5 11217  hoaddcl 11321  homulcl 11322  homulid2 11363  homco1 11364  homulass 11365  hoadddi 11366  hoadddir 11367  hoeq1 11393  hoeq2 11394  adjsym 11396  nmopsetretALT 11427  nmfnsetre 11441  cnvadj 11453  hhlnoi 11463  nmopub2tALT 11470  nmopge0 11472  unopf1o 11477  unopnorm 11478  cnvunop 11479  unopadj 11480  unoplin 11481  counop 11482  hmopre 11484  nmfnleub2 11487  nmfnge0 11488  adjcl 11493  adj2 11495  hmoplin 11503  bracl 11510  eigvalcl 11522  lnop0 11527  lnopmul 11528  homco2 11538  hmops 11582  hmopm 11583  hmopco 11585  nlelchi 11631  adjlnop 11656  adjmul 11662  adjadd 11663  leop2 11695  leopsq 11700  leopadd 11703  leopmuli 11704  leopnmid 11709  hmopidmchi 11723  pjinvari 11764  stcl 11788  hstcl 11789  fseq1cl 13619  ghomgrpilem2 13629  ghomcl 13635  nn0seqcvgd 13659  algrp1 13742  alginv 13743  algcvg 13744  algcvga 13747  algfx 13748  eucalgcvga 13754  eucalg 13755  soseq 13955  njtlc 14389  surjsec 14462  fopab2g 14485  valcurfn 14551  seqzp2 14716  usptoplem 14917  istopx 14918  prtoptop 14919  conttnf 14944  cntrsetlem 14999  lvsovso 15038  lvsovso2 15039  idmoa 15078  rdmob 15095  dmrngcmp 15098  dmo 15123  cdmo 15124  jdmo 15125  mrdmcd 15143  finsschain 15373  ordisoOLD 15374  hartogOLD 15384  hscptsscld 15434  alexsublem3 15439  cnpfillim 15589  fcluscomplem 15620  filnetlem5 15644  filnet 15645  foco2 15686  upixp 15729  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seqpo 15814  incsequz 15815  incsequz2 15816  metf1o 15843  mettrifi2 15848  geomcau 15849  lmclim2 15850  lmtlm 15908  ismtyhmeolem 15950  heiborlem30 15984  heiborlem31 15985  heiborlem32 15986  heiborlem33 15987  heiborlem35 15989  heiborlem36 15990  heiborlem39 15993  bfplem4 16001  rrnmet 16016  rrndstprj1 16017  rrndstprj2 16018  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  ghomco 16040  ghomdiv 16041  grpkerinj 16042  phtpycolem5 16055  reparpht 16065  pcocn 16076  pcopt 16084  pcorev 16087  rnghomcl 16121  smofvon 16450

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014

Copyright terms: Public domain