Theorem fnfvima 7181

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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  7182  isomin  7285  isofrlem  7288  fnwelem  8074  fimaproj  8078  php3  9136  fissuni  9260  unxpwdom2  9496  cantnflt  9584  dfac12lem2  10058  ackbij2  10155  isf34lem7  10292  isf34lem6  10293  zorn2lem2  10410  ttukeylem5  10426  tskuni  10697  axpre-sup  11083  limsupval2  15433  mgmhmima  18674  mhmimalem  18783  mhmima  18784  ghmnsgima  19206  psgnunilem1  19459  dprdfeq0  19990  dprd2dlem1  20009  rhmimasubrnglem  20533  lmhmima  21034  lmcnp  23279  basqtop  23686  tgqtop  23687  kqfvima  23705  reghmph  23768  uzrest  23872  qustgpopn  24095  qustgplem  24096  cphsqrtcl  25161  lhop  25993  ig1peu  26150  ig1pdvds  26155  plypf1  26187  nosupno  27681  nosupbday  27683  noinfno  27696  noinfbday  27698  noetasuplem4  27714  noetainflem4  27718  eqcuts2  27792  cutsun12  27796  cutbdaybnd  27801  cutbdaybnd2  27802  cutbdaylt  27804  madebdaylemlrcut  27905  sltsbday  27923  cofcut1  27926  cofcutr  27930  lrrecfr  27949  negsproplem4  28037  negsproplem5  28038  negsproplem6  28039  f1otrg  28953  txomap  33994  sitgaddlemb  34508  f1resrcmplf1dlem  35245  noinfepfnregs  35292  cvmopnlem  35476  mrsubrn  35711  msubrn  35727  ttcid  36690  dfttc2g  36704  regsfromunir1  36738  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem23  37978  cnambfre  38003  ftc1anclem7  38034  ftc1anc  38036  aks6d1c2  42583  aks6d1c7lem1  42633  isnumbasgrplem1  43547  relpmin  45397  relpfrlem  45398  permaxun  45456  funimaeq  45693