Theorem fnfvima 7221

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 6625	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1149	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1153	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6628	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1149	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3976	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 520	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1154	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7219	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 66	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907  dom cdm 5652   “ cima 5655  Fun wfun 6519   Fn wfn 6520  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-fv 6533

This theorem is referenced by:  fnfvimad  7222  isomin  7325  isofrlem  7328  fnwelem  8115  fimaproj  8119  php3  9181  fissuni  9302  unxpwdom2  9538  cantnflt  9629  dfac12lem2  10116  ackbij2  10213  isf34lem7  10351  isf34lem6  10352  zorn2lem2  10469  ttukeylem5  10485  tskuni  10756  axpre-sup  11142  limsupval2  15521  mgmhmima  18763  mhmimalem  18873  mhmima  18874  ghmnsgima  19301  psgnunilem1  19554  dprdfeq0  20085  dprd2dlem1  20104  rhmimasubrnglem  20641  lmhmima  21137  lmcnp  23422  basqtop  23829  tgqtop  23830  kqfvima  23848  reghmph  23911  uzrest  24015  qustgpopn  24238  qustgplem  24239  cphsqrtcl  25304  lhop  26136  ig1peu  26293  ig1pdvds  26298  plypf1  26330  nosupno  27825  nosupbday  27827  noinfno  27840  noinfbday  27842  noetasuplem4  27858  noetainflem4  27862  eqcuts2  27937  cutsun12  27941  cutbdaybnd  27946  cutbdaybnd2  27947  cutbdaylt  27949  madebdaylemlrcut  28050  sltsbday  28068  cofcut1  28071  cofcutr  28075  lrrecfr  28094  negsproplem4  28182  negsproplem5  28183  negsproplem6  28184  f1otrg  29129  txomap  34141  sitgaddlemb  34655  f1resrcmplf1dlem  35390  noinfepfnregs  35440  cvmopnlem  35641  mrsubrn  35876  msubrn  35892  ttcid  36865  dfttc2g  36879  regsfromunir1  36913  poimirlem4  38135  poimirlem6  38137  poimirlem7  38138  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem23  38154  cnambfre  38179  ftc1anclem7  38210  ftc1anc  38212  aks6d1c2  42759  aks6d1c7lem1  42809  isnumbasgrplem1  43690  relpmin  45526  relpfrlem  45527  permaxun  45585  funimaeq  45819