Theorem fnfvima 7236

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 6636	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1151	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1155	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6639	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1151	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3971	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 521	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1156	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7234	. 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 3902  dom cdm 5659   “ cima 5662  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  fnfvimad  7237  f1resrcmplf1dlem  7275  isomin  7342  isofrlem  7345  fnwelem  8133  fimaproj  8137  php3  9207  fissuni  9328  unxpwdom2  9564  cantnflt  9655  dfac12lem2  10151  ackbij2  10248  isf34lem7  10385  isf34lem6  10386  zorn2lem2  10503  ttukeylem5  10519  tskuni  10796  axpre-sup  11182  limsupval2  15571  mgmhmima  18823  mhmimalem  18939  mhmima  18940  ghmnsgima  19373  psgnunilem1  19626  dprdfeq0  20157  dprd2dlem1  20176  rhmimasubrnglem  20733  lmhmima  21237  lmcnp  23535  basqtop  23943  tgqtop  23944  kqfvima  23962  reghmph  24025  uzrest  24129  qustgpopn  24352  qustgplem  24353  cphsqrtcl  25418  lhop  26250  ig1peu  26407  ig1pdvds  26412  plypf1  26445  nosupno  27947  nosupbday  27949  noinfno  27962  noinfbday  27964  noetasuplem4  27980  noetainflem4  27984  eqcuts2  28059  cutsun12  28063  cutbdaybnd  28068  cutbdaybnd2  28069  cutbdaylt  28071  madebdaylemlrcut  28172  sltsbday  28190  cofcut1  28193  cofcutr  28197  lrrecfr  28216  negsproplem4  28304  negsproplem5  28305  negsproplem6  28306  f1otrg  29335  txomap  34352  sitgaddlemb  34867  fnfvintima  35599  dfscott3  35634  noinfepfnregs  35666  cvmopnlem  35865  mrsubrn  36100  msubrn  36116  ttcid  37119  dfttc2g  37133  regsfromunir1  37167  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem23  38400  cnambfre  38425  ftc1anclem7  38456  ftc1anc  38458  aks6d1c2  43004  aks6d1c7lem1  43054  isnumbasgrplem1  43950  relpmin  45783  relpfrlem  45784  permaxun  45842  funimaeq  46083