Theorem ffvelrn 3814

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 3813	. . 3 |- ((F Fn A /\ C e. A) -> (F` C) e. ran F)
2		ffn 3627	. . 3 |- (F:A-->B -> F Fn A)
3	1, 2	sylan 448	. 2 |- ((F:A-->B /\ C e. A) -> (F` C) e. ran F)
4		frn 3633	. . . 4 |- (F:A-->B -> ran F (_ B)
5	4	sseld 2067	. . 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 223   e. wcel 958  ran crn 3171   Fn wfn 3177  -->wf 3178  ` cfv 3182

This theorem is referenced by:  ffvelrni 3815  dffo3 3819  fopab2 3823  ffnfv 3828  fopabco 3832  fsn2 3836  fvconst 3839  f1ocnvfv3 3883  f1ocnvdm 3884  isocnv 3896  isotr 3897  isotrALT 3898  foprrn 4035  omsmolem 4256  omsmo 4257  2dom 4427  xpdom2 4442  pw2en 4446  mapenlem2 4490  mapxpen 4495  xpmapenlem3 4498  xpmapenlem4 4499  xpmapenlem5 4500  unifiOLD 4557  fiint 4559  fiintOLD 4560  unidom 4808  seq1rn2 6321  seq1rn 6322  seq1cl 6325  seq1cl2 6326  ser1recl 6331  fsequb2 6524  seqzrn2 6556  seqzrn 6557  seq1bnd 6910  clm4f 7082  climfnn 7092  climubi 7153  infcvglem3 7223  cncffvelrnOLD 7267  cncffvelrn 7268  efseq0ex 7311  acdc3lem 7486  acdclem 7494  acdcALT 7496  ruclem13 7522  ruclem15 7524  ruclem22 7531  ruclem23 7532  ruclem24 7533  ruclem25 7534  ruclem26 7535  ruclem27 7536  ruclem28 7537  ruclem29 7538  cnpcl 7764  cnpco 7769  metcnplem 7886  metcnp 7887  metcnp2 7888  metcnpi3 7892  metcnpi4 7893  metcni2 7895  metcnss 7898  cncfmet 7905  lmbrf 7930  lmnn 7935  iscauf 7939  iscau5 7941  iscaunns 7944  lmss 7953  causs 7955  metelcls 7965  metcnp4 7970  xplmi 7973  xpcn 7976  oprcn 7977  bopcnlem2 7982  bopcnlem4 7984  cncms 7998  bcthlem4 8002  bcthlem16 8014  bcthlem17 8015  bcthlem18 8016  bcthlem33 8031  nvcl 8287  nvcni 8329  nvcni2 8330  nvcni3 8331  nvlmle 8333  sqcn 8335  lno0 8417  lnoadd 8419  lnosub 8420  lnomul 8421  nvcnpi3 8422  nvcnpi4 8423  nmosetre 8427  nmoge0 8430  nmoub3i 8436  nmounbi 8439  blometi 8463  phoeqi 8518  ubthlem3 8531  ubthlem5 8533  ubthlem11 8539  ubthlem12 8540  minveclem4 8548  minveclem9 8553  minveclem16 8560  minveclem17 8561  minveclem28 8572  htthlem1 8620  htthlem5 8624  htthlem6 8625  htthlem8 8627  htthlem9 8628  h2hcau 8849  h2hlm 8850  hcau2 9055  hhcms 9072  hhsscms 9150  occllem4 9176  occllem6 9178  occl 9181  projlem21 9206  projlem24 9209  projlem25 9210  projlem26 9211  hosclt 9523  homclt 9524  hodclt 9525  osumlem4 9581  osumlem5 9582  hoaddclt 9684  homulclt 9685  homulid2t 9726  homco1t 9727  homulasst 9728  hoadddit 9729  hoadddirt 9730  hoeq1t 9756  hoeq2t 9757  adjsymt 9759  nmopsetretALT 9790  nmfnsetret 9804  cnvadj 9816  hhlno 9826  nmopub2tALT 9833  nmopge0t 9835  unopf1ot 9840  unopnormt 9841  cnvunopt 9842  unopadjt 9843  unoplint 9844  counopt 9845  hmopret 9847  nmfnleub2t 9850  nmfnge0t 9851  adjclt 9856  adj2t 9858  hmoplint 9866  braclt 9873  eigvalclt 9885  lnop0t 9890  lnopmult 9891  homco2t 9901  hmopst 9945  hmopmt 9946  hmopcot 9948  nlelch 9994  adjlnopt 10019  adjmult 10025  adjaddt 10026  leop2t 10057  leopsqt 10062  leopaddt 10065  leopmulit 10066  leopnmidt 10071  hmopidmch 10079  pjinvar 10119  stclt 10143  hstclt 10144  ghomgrpilem2 10386  ghomcl 10392  ghomid 10394  idmoa 10664  rdmob 10681  dmo 10709  cdmo 10710  jdmo 10711  mrdmcd 10722  homib 10724  iri 10728

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-id 2835  df-xp 3184  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198

Copyright terms: Public domain