Theorem fnfvima 7231

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 6631	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1151	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1155	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6634	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1151	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3968	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 521	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1156	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7229	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 66	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  dom cdm 5651   “ cima 5654  Fun wfun 6525   Fn wfn 6526  ‘cfv 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is used by:  fnfvimad  7232  f1resrcmplf1dlem  7270  isomin  7337  isofrlem  7340  fnwelem  8132  fimaproj  8136  php3  9208  fissuni  9330  unxpwdom2  9566  cantnflt  9657  dfac12lem2  10204  ackbij2  10301  isf34lem7  10438  isf34lem6  10439  zorn2lem2  10556  ttukeylem5  10572  tskuni  10849  axpre-sup  11235  limsupval2  15627  mgmhmima  18884  mhmimalem  19000  mhmima  19001  ghmnsgima  19434  psgnunilem1  19687  dprdfeq0  20218  dprd2dlem1  20237  rhmimasubrnglem  20797  lmhmima  21302  lmcnp  23602  basqtop  24010  tgqtop  24011  kqfvima  24029  reghmph  24092  uzrest  24196  qustgpopn  24419  qustgplem  24420  cphsqrtcl  25485  lhop  26316  ig1peu  26473  ig1pdvds  26478  plypf1  26511  nosupno  28042  nosupbday  28044  noinfno  28057  noinfbday  28059  noetasuplem4  28075  noetainflem4  28079  eqcuts2  28154  cutsun12  28158  cutbdaybnd  28163  cutbdaybnd2  28164  cutbdaylt  28166  madebdaylemlrcut  28267  sltsbday  28285  cofcut1  28288  cofcutr  28292  lrrecfr  28311  negsproplem4  28399  negsproplem5  28400  negsproplem6  28401  f1otrg  29430  txomap  34448  sitgaddlemb  34963  fnfvintima  35695  dfscott3  35721  noinfepfnregs  35773  cvmopnlem  36012  mrsubrn  36247  msubrn  36263  ttcid  37250  dfttc2g  37264  regsfromunir1  37298  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem23  38529  cnambfre  38554  ftc1anclem7  38585  ftc1anc  38587  aks6d1c2  43148  aks6d1c7lem1  43198  isnumbasgrplem1  44061  relpmin  45894  relpfrlem  45895  permaxun  45953  funimaeq  46201