Theorem fnfvima 7173

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ⊆ wss 3905  dom cdm 5623   “ cima 5626  Fun wfun 6480   Fn wfn 6481  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-fv 6494

This theorem is referenced by:  fnfvimad  7174  isomin  7278  isofrlem  7281  fnwelem  8071  fimaproj  8075  php3  9133  fissuni  9266  unxpwdom2  9499  cantnflt  9587  dfac12lem2  10058  ackbij2  10155  isf34lem7  10292  isf34lem6  10293  zorn2lem2  10410  ttukeylem5  10426  tskuni  10696  axpre-sup  11082  limsupval2  15405  mgmhmima  18607  mhmimalem  18716  mhmima  18717  ghmnsgima  19137  psgnunilem1  19390  dprdfeq0  19921  dprd2dlem1  19940  rhmimasubrnglem  20468  lmhmima  20969  lmcnp  23207  basqtop  23614  tgqtop  23615  kqfvima  23633  reghmph  23696  uzrest  23800  qustgpopn  24023  qustgplem  24024  cphsqrtcl  25100  lhop  25937  ig1peu  26096  ig1pdvds  26101  plypf1  26133  nosupno  27631  nosupbday  27633  noinfno  27646  noinfbday  27648  noetasuplem4  27664  noetainflem4  27668  eqscut2  27735  scutun12  27739  scutbdaybnd  27744  scutbdaybnd2  27745  scutbdaylt  27747  madebdaylemlrcut  27831  cofcut1  27851  cofcutr  27855  lrrecfr  27873  negsproplem4  27960  negsproplem5  27961  negsproplem6  27962  f1otrg  28834  txomap  33800  sitgaddlemb  34315  f1resrcmplf1dlem  35052  cvmopnlem  35250  mrsubrn  35485  msubrn  35501  poimirlem4  37603  poimirlem6  37605  poimirlem7  37606  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem23  37622  cnambfre  37647  ftc1anclem7  37678  ftc1anc  37680  aks6d1c2  42103  aks6d1c7lem1  42153  isnumbasgrplem1  43074  relpmin  44926  relpfrlem  44927  permaxun  44985  funimaeq  45224