Theorem ffvelrn 3805

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 3804	. . 3 |- ((F Fn A /\ C e. A) -> (F` C) e. ran F)
2		ffn 3619	. . 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 3624	. . . 4 |- (F:A-->B -> ran F (_ B)
5	4	sseld 2063	. . 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 956  ran crn 3166   Fn wfn 3172  -->wf 3173  ` cfv 3177

This theorem is referenced by:  ffvelrni 3806  dffo3 3810  fopab2 3814  ffnfv 3819  fopabco 3823  fsn2 3827  fvconst 3830  f1ocnvfv3 3874  f1ocnvdm 3875  isocnv 3887  isotr 3888  isotrALT 3889  foprrn 4026  omsmolem 4246  omsmo 4247  2dom 4414  xpdom2 4428  pw2en 4432  mapenlem2 4476  mapxpen 4481  xpmapenlem3 4484  xpmapenlem4 4485  xpmapenlem5 4486  unifi 4538  fiint 4540  unidom 4788  seq1rn2 6266  seq1rn 6267  seq1cl 6270  seq1cl2 6271  ser1recl 6276  fsequb2 6464  seqzrn2 6496  seqzrn 6497  seq1bnd 6855  clm4f 7028  climfnn 7038  climubi 7097  infcvglem3 7166  cncffvelrnOLD 7210  cncffvelrn 7211  efseq0ex 7261  acdc3lem 7436  acdclem 7444  acdcALT 7446  ruclem13 7473  ruclem15 7475  ruclem22 7482  ruclem23 7483  ruclem24 7484  ruclem25 7485  ruclem26 7486  ruclem27 7487  ruclem28 7488  ruclem29 7489  cnpcl 7714  cnpco 7719  metcnplem 7838  metcnp 7839  metcnp2 7840  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnss 7850  cncfmet 7857  lmbrf 7882  lmnn 7887  iscauf 7891  iscau5 7893  lmss 7904  causs 7906  metelcls 7916  metcnp4 7920  xplmi 7923  xpcn 7926  oprcn 7927  bopcnlem2 7932  bopcnlem4 7934  cncms 7948  bcthlem4 7952  bcthlem16 7964  bcthlem17 7965  bcthlem18 7966  bcthlem33 7981  nvcl 8239  nvcni 8279  nvlmle 8281  sqcn 8283  lno0 8364  lnosub 8366  lnomul 8367  nvcnpi4 8368  nmosetre 8372  nmoge0 8375  nmoub3i 8381  nmounbi 8384  blometi 8407  phoeqi 8462  ubthlem3 8475  ubthlem5 8477  ubthlem11 8483  ubthlem12 8484  minveclem4 8492  minveclem9 8497  minveclem16 8504  minveclem17 8505  minveclem28 8516  htthlem1 8563  htthlem5 8567  htthlem6 8568  htthlem8 8570  htthlem9 8571  h2hcau 8788  h2hlm 8789  hcau2 8994  hhcms 9011  hhsscms 9089  occllem4 9115  occllem6 9117  occl 9120  projlem21 9145  projlem24 9148  projlem25 9149  projlem26 9150  hosclt 9463  homclt 9464  hodclt 9465  osumlem4 9521  osumlem5 9522  hoaddclt 9624  homulclt 9625  homulid2t 9666  homco1t 9667  homulasst 9668  hoadddit 9669  hoadddirt 9670  hoeq1t 9696  hoeq2t 9697  adjsymt 9699  nmopsetretALT 9730  nmfnsetret 9744  cnvadj 9756  hhlno 9766  nmopub2tALT 9773  nmopge0t 9774  unopf1ot 9779  unopnormt 9780  cnvunopt 9781  unopadjt 9782  unoplint 9783  counopt 9784  hmopret 9786  nmfnleub2t 9789  nmfnge0t 9790  adjclt 9795  adj2t 9797  hmoplint 9805  braclt 9812  eigvalclt 9824  lnop0t 9829  lnopmult 9830  homco2t 9840  hmopst 9883  hmopmt 9884  hmopcot 9886  nlelch 9932  adjlnopt 9957  adjmult 9963  adjaddt 9964  leop2t 9995  leopsqt 10000  leopaddt 10003  leopmulit 10004  leopnmidt 10009  hmopidmch 10017  pjinvar 10057  stclt 10081  hstclt 10082  ghomgrpilem2 10320  ghomcl 10326  ghomid 10328  idmoa 10544  rdmob 10561  dmo 10589  cdmo 10590  jdmo 10591  mrdmcd 10602  homib 10604  iri 10608

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-id 2830  df-xp 3179  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193

Copyright terms: Public domain