Theorem ffvelrn 3890

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 3889	. . 3 |- ((F Fn A /\ C e. A) -> (F` C) e. ran F)
2		ffn 3702	. . 3 |- (F:A-->B -> F Fn A)
3	1, 2	sylan 450	. 2 |- ((F:A-->B /\ C e. A) -> (F` C) e. ran F)
4		frn 3708	. . . 4 |- (F:A-->B -> ran F (_ B)
5	4	sseld 2111	. . 3 |- (F:A-->B -> ((F` C) e. ran F -> (F` C) e. B))
6	5	adantr 389	. 2 |- ((F:A-->B /\ C e. A) -> ((F` C) e. ran F -> (F` C) e. B))
7	3, 6	mpd 26	1 |- ((F:A-->B /\ C e. A) -> (F` C) e. B)

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 990  ran crn 3226   Fn wfn 3232  -->wf 3233  ` cfv 3237

This theorem is referenced by:  ffvelrni 3891  dffo3 3895  fopab2 3899  ffnfv 3904  fopabco 3908  fsn2 3912  fvconst 3915  f1ocnvfv3 3959  f1ocnvdm 3960  isocnv 3972  isotr 3973  isotrALT 3974  foprrn 4113  omsmolem 4340  omsmo 4341  2dom 4514  xpdom2 4529  pw2en 4533  mapenlem2 4579  mapxpen 4584  xpmapenlem3 4587  xpmapenlem4 4588  xpmapenlem5 4589  unifi 4642  fiint 4644  unidom 4894  fsequb2 6584  seq1rn2 6614  seq1rn 6615  seq1cl 6618  seq1cl2 6619  ser1recli 6624  seqzrn2 6679  seqzrn 6680  seq1bndi 7033  clm4fi 7205  climfnn 7215  climubii 7276  infcvglem3 7346  cncffvelrnOLD 7390  cncffvelrn 7391  efseq0ex 7434  acdc3lem 7611  acdclem 7619  acdcALT 7621  ruclem13 7647  ruclem15 7649  ruclem22 7656  ruclem23 7657  ruclem24 7658  ruclem25 7659  ruclem26 7660  ruclem27 7661  ruclem28 7662  ruclem29 7663  cnpcl 7884  cnpco 7889  metcnplem 8006  metcnp 8007  metcnp2 8008  metcnpi3 8012  metcnpi4 8013  metcni2 8015  metcnss 8018  cncfmet 8025  lmbrf 8050  lmnn 8055  iscauf 8059  iscau5 8061  iscaunns 8064  lmss 8073  causs 8075  metelcls 8085  metcnp4 8090  xplmi 8093  xpcn 8096  oprcn 8097  bopcnlem2 8102  bopcnlem4 8104  cncms 8118  bcthlem4 8122  bcthlem16 8134  bcthlem17 8135  bcthlem18 8136  bcthlem33 8151  nvcl 8406  nvcni 8448  nvcni2 8449  nvcni3 8450  nvlmle 8452  sqcn 8454  lno0 8536  lnoadd 8538  lnosub 8539  lnomul 8540  nvcnpi3 8541  nvcnpi4 8542  nmosetre 8546  nmoge0 8549  nmoub3i 8555  nmounbi 8558  blometi 8582  phoeqi 8637  ubthlem3 8650  ubthlem5 8652  ubthlem11 8658  ubthlem12 8659  minveclem4 8667  minveclem9 8672  minveclem16 8679  minveclem17 8680  minveclem28 8691  htthlem1 8739  htthlem5 8743  htthlem6 8744  htthlem8 8746  htthlem9 8747  h2hcau 8968  h2hlm 8969  hcau2 9175  hhcms 9192  hhsscms 9270  occllem4 9296  occllem6 9298  occli 9301  projlem21 9326  projlem24 9329  projlem25 9330  projlem26 9331  hoscl 9643  homcl 9644  hodcl 9645  osumlem4 9701  osumlem5 9702  hoaddcl 9804  homulcl 9805  homulid2 9846  homco1 9847  homulass 9848  hoadddi 9849  hoadddir 9850  hoeq1 9876  hoeq2 9877  adjsym 9879  nmopsetretALT 9908  nmfnsetre 9922  cnvadj 9934  hhlnoi 9944  nmopub2tALT 9951  nmopge0 9953  unopf1o 9958  unopnorm 9959  cnvunop 9960  unopadj 9961  unoplin 9962  counop 9963  hmopre 9965  nmfnleub2 9968  nmfnge0 9969  adjcl 9974  adj2 9976  hmoplin 9984  bracl 9991  eigvalcl 10003  lnop0 10007  lnopmul 10008  homco2 10018  hmops 10062  hmopm 10063  hmopco 10065  nlelchi 10111  adjlnop 10136  adjmul 10142  adjadd 10143  leop2 10174  leopsq 10179  leopadd 10182  leopmuli 10183  leopnmid 10188  hmopidmchi 10196  pjinvari 10237  stcl 10261  hstcl 10262  ghomgrpilem2 10507  ghomcl 10513  ghomid 10515  idmoa 10799  rdmob 10816  dmo 10844  cdmo 10845  jdmo 10846  mrdmcd 10857

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-fv 3253

Copyright terms: Public domain