Theorem fnfvima 7176

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ⊆ wss 3899  dom cdm 5621   “ cima 5624  Fun wfun 6483   Fn wfn 6484  ‘cfv 6489

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 2182  ax-ext 2705  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 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  fnfvimad  7177  isomin  7280  isofrlem  7283  fnwelem  8070  fimaproj  8074  php3  9128  fissuni  9251  unxpwdom2  9484  cantnflt  9572  dfac12lem2  10046  ackbij2  10143  isf34lem7  10280  isf34lem6  10281  zorn2lem2  10398  ttukeylem5  10414  tskuni  10684  axpre-sup  11070  limsupval2  15397  mgmhmima  18633  mhmimalem  18742  mhmima  18743  ghmnsgima  19162  psgnunilem1  19415  dprdfeq0  19946  dprd2dlem1  19965  rhmimasubrnglem  20490  lmhmima  20991  lmcnp  23229  basqtop  23636  tgqtop  23637  kqfvima  23655  reghmph  23718  uzrest  23822  qustgpopn  24045  qustgplem  24046  cphsqrtcl  25121  lhop  25958  ig1peu  26117  ig1pdvds  26122  plypf1  26154  nosupno  27652  nosupbday  27654  noinfno  27667  noinfbday  27669  noetasuplem4  27685  noetainflem4  27689  eqscut2  27757  scutun12  27761  scutbdaybnd  27766  scutbdaybnd2  27767  scutbdaylt  27769  madebdaylemlrcut  27854  cofcut1  27874  cofcutr  27878  lrrecfr  27896  negsproplem4  27983  negsproplem5  27984  negsproplem6  27985  f1otrg  28859  txomap  33858  sitgaddlemb  34372  f1resrcmplf1dlem  35109  cvmopnlem  35333  mrsubrn  35568  msubrn  35584  poimirlem4  37674  poimirlem6  37676  poimirlem7  37677  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem23  37693  cnambfre  37718  ftc1anclem7  37749  ftc1anc  37751  aks6d1c2  42233  aks6d1c7lem1  42283  isnumbasgrplem1  43208  relpmin  45059  relpfrlem  45060  permaxun  45118  funimaeq  45357