Theorem fnfvima 7179

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  dom cdm 5624   “ cima 5627  Fun wfun 6486   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  fnfvimad  7180  isomin  7283  isofrlem  7286  fnwelem  8073  fimaproj  8077  php3  9133  fissuni  9257  unxpwdom2  9493  cantnflt  9581  dfac12lem2  10055  ackbij2  10152  isf34lem7  10289  isf34lem6  10290  zorn2lem2  10407  ttukeylem5  10423  tskuni  10694  axpre-sup  11080  limsupval2  15403  mgmhmima  18640  mhmimalem  18749  mhmima  18750  ghmnsgima  19169  psgnunilem1  19422  dprdfeq0  19953  dprd2dlem1  19972  rhmimasubrnglem  20498  lmhmima  20999  lmcnp  23248  basqtop  23655  tgqtop  23656  kqfvima  23674  reghmph  23737  uzrest  23841  qustgpopn  24064  qustgplem  24065  cphsqrtcl  25140  lhop  25977  ig1peu  26136  ig1pdvds  26141  plypf1  26173  nosupno  27671  nosupbday  27673  noinfno  27686  noinfbday  27688  noetasuplem4  27704  noetainflem4  27708  eqcuts2  27782  cutsun12  27786  cutbdaybnd  27791  cutbdaybnd2  27792  cutbdaylt  27794  madebdaylemlrcut  27895  sltsbday  27913  cofcut1  27916  cofcutr  27920  lrrecfr  27939  negsproplem4  28027  negsproplem5  28028  negsproplem6  28029  f1otrg  28943  txomap  33991  sitgaddlemb  34505  f1resrcmplf1dlem  35242  noinfepfnregs  35288  cvmopnlem  35472  mrsubrn  35707  msubrn  35723  regsfromunir1  36670  poimirlem4  37821  poimirlem6  37823  poimirlem7  37824  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem23  37840  cnambfre  37865  ftc1anclem7  37896  ftc1anc  37898  aks6d1c2  42380  aks6d1c7lem1  42430  isnumbasgrplem1  43339  relpmin  45189  relpfrlem  45190  permaxun  45248  funimaeq  45486