Theorem fnfvima 6818

Description: The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015.)

Assertion

Ref	Expression
fnfvima	⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Proof of Theorem fnfvima

Step	Hyp	Ref	Expression
1		fnfun 6283	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1114	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1118	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6285	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1114	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtr4d 3891	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 504	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1119	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 6817	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051   ⊆ wss 3822  dom cdm 5403   “ cima 5406  Fun wfun 6179   Fn wfn 6180  ‘cfv 6185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-sep 5056  ax-nul 5063  ax-pr 5182

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-sbc 3675  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-iota 6149  df-fun 6187  df-fn 6188  df-fv 6193

This theorem is referenced by:  fnfvimad  6819  isomin  6911  isofrlem  6914  fnwelem  7628  php3  8497  fissuni  8622  unxpwdom2  8845  cantnflt  8927  dfac12lem2  9362  ackbij2  9461  isf34lem7  9597  isf34lem6  9598  zorn2lem2  9715  ttukeylem5  9731  tskuni  10001  axpre-sup  10387  limsupval2  14696  mhmima  17843  ghmnsgima  18165  psgnunilem1  18394  dprdfeq0  18906  dprd2dlem1  18925  lmhmima  19553  lmcnp  21631  basqtop  22038  tgqtop  22039  kqfvima  22057  reghmph  22120  uzrest  22224  qustgpopn  22446  qustgplem  22447  cphsqrtcl  23506  lhop  24331  ig1peu  24483  ig1pdvds  24488  plypf1  24520  f1otrg  26375  fimaproj  30773  txomap  30774  sitgaddlemb  31283  f1resrcmplf1dlem  32026  cvmopnlem  32147  mrsubrn  32317  msubrn  32333  nosupno  32761  nosupbday  32763  noetalem3  32777  scutun12  32829  scutbdaybnd  32833  scutbdaylt  32834  poimirlem4  34374  poimirlem6  34376  poimirlem7  34377  poimirlem16  34386  poimirlem17  34387  poimirlem19  34389  poimirlem20  34390  poimirlem23  34393  cnambfre  34418  ftc1anclem7  34451  ftc1anc  34453  isnumbasgrplem1  39135  funimaeq  40978  mgmhmima  43469