Theorem fnfvima 7239

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  dom cdm 5650   “ cima 5653  Fun wfun 6532   Fn wfn 6533  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  fnfvimad  7240  f1resrcmplf1dlem  7278  isomin  7345  isofrlem  7348  fnwelem  8145  fimaproj  8154  php3  9227  fissuni  9349  unxpwdom2  9585  cantnflt  9676  dfac12lem2  10226  ackbij2  10323  isf34lem7  10460  isf34lem6  10461  zorn2lem2  10578  ttukeylem5  10594  tskuni  10871  axpre-sup  11257  limsupval2  15652  mgmhmima  18909  mhmimalem  19025  mhmima  19026  ghmnsgima  19459  psgnunilem1  19712  dprdfeq0  20243  dprd2dlem1  20262  rhmimasubrnglem  20822  lmhmima  21327  lmcnp  23627  basqtop  24035  tgqtop  24036  kqfvima  24054  reghmph  24117  uzrest  24221  qustgpopn  24444  qustgplem  24445  cphsqrtcl  25510  lhop  26341  ig1peu  26498  ig1pdvds  26503  plypf1  26536  nosupno  28065  nosupbday  28067  noinfno  28080  noinfbday  28082  noetasuplem4  28098  noetainflem4  28102  eqcuts2  28177  cutsun12  28181  cutbdaybnd  28186  cutbdaybnd2  28187  cutbdaylt  28189  madebdaylemlrcut  28290  sltsbday  28308  cofcut1  28311  cofcutr  28315  lrrecfr  28334  negsproplem4  28422  negsproplem5  28423  negsproplem6  28424  f1otrg  29453  txomap  34512  sitgaddlemb  35026  fnfvintima  35762  dfscott3  35797  noinfepfnregs  35856  cvmopnlem  36129  mrsubrn  36364  msubrn  36380  ttcid  37372  dfttc2g  37386  regsfromunir1  37420  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem23  38654  cnambfre  38679  ftc1anclem7  38710  ftc1anc  38712  aks6d1c2  43273  aks6d1c7lem1  43323  isnumbasgrplem1  44196  relpmin  46035  relpfrlem  46036  permaxun  46094  funimaeq  46351