Theorem fnfvima 7219

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 6638	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1133	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1137	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6641	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1133	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 4019	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 512	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1138	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7217	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ⊆ wss 3944  dom cdm 5669   “ cima 5672  Fun wfun 6526   Fn wfn 6527  ‘cfv 6532

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-fv 6540

This theorem is referenced by:  fnfvimad  7220  isomin  7318  isofrlem  7321  fnwelem  8099  fimaproj  8103  php3  9195  php3OLD  9207  fissuni  9340  unxpwdom2  9565  cantnflt  9649  dfac12lem2  10121  ackbij2  10220  isf34lem7  10356  isf34lem6  10357  zorn2lem2  10474  ttukeylem5  10490  tskuni  10760  axpre-sup  11146  limsupval2  15406  mhmima  18681  ghmnsgima  19082  psgnunilem1  19325  dprdfeq0  19851  dprd2dlem1  19870  lmhmima  20607  lmcnp  22737  basqtop  23144  tgqtop  23145  kqfvima  23163  reghmph  23226  uzrest  23330  qustgpopn  23553  qustgplem  23554  cphsqrtcl  24630  lhop  25462  ig1peu  25618  ig1pdvds  25623  plypf1  25655  nosupno  27133  nosupbday  27135  noinfno  27148  noinfbday  27150  noetasuplem4  27166  noetainflem4  27170  eqscut2  27233  scutun12  27237  scutbdaybnd  27242  scutbdaybnd2  27243  scutbdaylt  27245  madebdaylemlrcut  27316  cofcut1  27327  cofcutr  27331  lrrecfr  27343  negsproplem4  27421  negsproplem5  27422  negsproplem6  27423  f1otrg  27987  txomap  32645  sitgaddlemb  33178  f1resrcmplf1dlem  33920  cvmopnlem  34100  mrsubrn  34335  msubrn  34351  poimirlem4  36296  poimirlem6  36298  poimirlem7  36299  poimirlem16  36308  poimirlem17  36309  poimirlem19  36311  poimirlem20  36312  poimirlem23  36315  cnambfre  36340  ftc1anclem7  36371  ftc1anc  36373  isnumbasgrplem1  41614  funimaeq  43723  mgmhmima  46344