Theorem fnfvima 7233

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 6637	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1151	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1155	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6640	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1151	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3975	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 520	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1156	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7231	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 66	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906  dom cdm 5663   “ cima 5666  Fun wfun 6532   Fn wfn 6533  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is referenced by:  fnfvimad  7234  isomin  7337  isofrlem  7340  fnwelem  8128  fimaproj  8132  php3  9194  fissuni  9315  unxpwdom2  9551  cantnflt  9642  dfac12lem2  10129  ackbij2  10226  isf34lem7  10364  isf34lem6  10365  zorn2lem2  10482  ttukeylem5  10498  tskuni  10769  axpre-sup  11155  limsupval2  15533  mgmhmima  18774  mhmimalem  18884  mhmima  18885  ghmnsgima  19311  psgnunilem1  19564  dprdfeq0  20095  dprd2dlem1  20114  rhmimasubrnglem  20651  lmhmima  21149  lmcnp  23442  basqtop  23849  tgqtop  23850  kqfvima  23868  reghmph  23931  uzrest  24035  qustgpopn  24258  qustgplem  24259  cphsqrtcl  25324  lhop  26156  ig1peu  26313  ig1pdvds  26318  plypf1  26350  nosupno  27845  nosupbday  27847  noinfno  27860  noinfbday  27862  noetasuplem4  27878  noetainflem4  27882  eqcuts2  27957  cutsun12  27961  cutbdaybnd  27966  cutbdaybnd2  27967  cutbdaylt  27969  madebdaylemlrcut  28070  sltsbday  28088  cofcut1  28091  cofcutr  28095  lrrecfr  28114  negsproplem4  28202  negsproplem5  28203  negsproplem6  28204  f1otrg  29198  txomap  34202  sitgaddlemb  34716  f1resrcmplf1dlem  35452  fnfvintima  35454  dfscott3  35490  noinfepfnregs  35523  cvmopnlem  35748  mrsubrn  35983  msubrn  35999  ttcid  36981  dfttc2g  36995  regsfromunir1  37029  poimirlem4  38253  poimirlem6  38255  poimirlem7  38256  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  poimirlem23  38272  cnambfre  38297  ftc1anclem7  38328  ftc1anc  38330  aks6d1c2  42875  aks6d1c7lem1  42925  isnumbasgrplem1  43808  relpmin  45641  relpfrlem  45642  permaxun  45700  funimaeq  45941