Theorem fnfvima 7238

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ⊆ wss 3908  dom cdm 5666   “ cima 5669  Fun wfun 6537   Fn wfn 6538  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-fv 6551

This theorem is used by:  fnfvimad  7239  f1resrcmplf1dlem  7279  isomin  7346  isofrlem  7349  fnwelem  8136  fimaproj  8140  php3  9203  fissuni  9324  unxpwdom2  9560  cantnflt  9651  dfac12lem2  10147  ackbij2  10244  isf34lem7  10381  isf34lem6  10382  zorn2lem2  10499  ttukeylem5  10515  tskuni  10786  axpre-sup  11172  limsupval2  15557  mgmhmima  18802  mhmimalem  18914  mhmima  18915  ghmnsgima  19341  psgnunilem1  19594  dprdfeq0  20125  dprd2dlem1  20144  rhmimasubrnglem  20701  lmhmima  21205  lmcnp  23498  basqtop  23905  tgqtop  23906  kqfvima  23924  reghmph  23987  uzrest  24091  qustgpopn  24314  qustgplem  24315  cphsqrtcl  25380  lhop  26212  ig1peu  26369  ig1pdvds  26374  plypf1  26406  nosupno  27904  nosupbday  27906  noinfno  27919  noinfbday  27921  noetasuplem4  27937  noetainflem4  27941  eqcuts2  28016  cutsun12  28020  cutbdaybnd  28025  cutbdaybnd2  28026  cutbdaylt  28028  madebdaylemlrcut  28129  sltsbday  28147  cofcut1  28150  cofcutr  28154  lrrecfr  28173  negsproplem4  28261  negsproplem5  28262  negsproplem6  28263  f1otrg  29257  txomap  34255  sitgaddlemb  34770  fnfvintima  35502  dfscott3  35537  noinfepfnregs  35569  cvmopnlem  35791  mrsubrn  36026  msubrn  36042  ttcid  37044  dfttc2g  37058  regsfromunir1  37092  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem23  38335  cnambfre  38360  ftc1anclem7  38391  ftc1anc  38393  aks6d1c2  42938  aks6d1c7lem1  42988  isnumbasgrplem1  43869  relpmin  45702  relpfrlem  45703  permaxun  45761  funimaeq  46002