Theorem fnfvima 7189

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 6600	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1134	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1138	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6603	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1134	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3973	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 511	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1139	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7187	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  dom cdm 5632   “ cima 5635  Fun wfun 6494   Fn wfn 6495  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  fnfvimad  7190  isomin  7293  isofrlem  7296  fnwelem  8083  fimaproj  8087  php3  9145  fissuni  9269  unxpwdom2  9505  cantnflt  9593  dfac12lem2  10067  ackbij2  10164  isf34lem7  10301  isf34lem6  10302  zorn2lem2  10419  ttukeylem5  10435  tskuni  10706  axpre-sup  11092  limsupval2  15415  mgmhmima  18652  mhmimalem  18761  mhmima  18762  ghmnsgima  19181  psgnunilem1  19434  dprdfeq0  19965  dprd2dlem1  19984  rhmimasubrnglem  20510  lmhmima  21011  lmcnp  23260  basqtop  23667  tgqtop  23668  kqfvima  23686  reghmph  23749  uzrest  23853  qustgpopn  24076  qustgplem  24077  cphsqrtcl  25152  lhop  25989  ig1peu  26148  ig1pdvds  26153  plypf1  26185  nosupno  27683  nosupbday  27685  noinfno  27698  noinfbday  27700  noetasuplem4  27716  noetainflem4  27720  eqcuts2  27794  cutsun12  27798  cutbdaybnd  27803  cutbdaybnd2  27804  cutbdaylt  27806  madebdaylemlrcut  27907  sltsbday  27925  cofcut1  27928  cofcutr  27932  lrrecfr  27951  negsproplem4  28039  negsproplem5  28040  negsproplem6  28041  f1otrg  28955  txomap  34011  sitgaddlemb  34525  f1resrcmplf1dlem  35261  noinfepfnregs  35307  cvmopnlem  35491  mrsubrn  35726  msubrn  35742  regsfromunir1  36689  poimirlem4  37869  poimirlem6  37871  poimirlem7  37872  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem23  37888  cnambfre  37913  ftc1anclem7  37944  ftc1anc  37946  aks6d1c2  42494  aks6d1c7lem1  42544  isnumbasgrplem1  43452  relpmin  45302  relpfrlem  45303  permaxun  45361  funimaeq  45598