Theorem fnfvima 7213

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 6617	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1145	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1149	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6620	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1145	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3973	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 519	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1150	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7211	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141   ⊆ wss 3904  dom cdm 5645   “ cima 5648  Fun wfun 6511   Fn wfn 6512  ‘cfv 6517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-fv 6525

This theorem is referenced by:  fnfvimad  7214  isomin  7317  isofrlem  7320  fnwelem  8106  fimaproj  8110  php3  9173  fissuni  9297  unxpwdom2  9533  cantnflt  9624  dfac12lem2  10098  ackbij2  10195  isf34lem7  10333  isf34lem6  10334  zorn2lem2  10451  ttukeylem5  10467  tskuni  10738  axpre-sup  11124  limsupval2  15490  mgmhmima  18732  mhmimalem  18841  mhmima  18842  ghmnsgima  19263  psgnunilem1  19516  dprdfeq0  20047  dprd2dlem1  20066  rhmimasubrnglem  20594  lmhmima  21094  lmcnp  23344  basqtop  23751  tgqtop  23752  kqfvima  23770  reghmph  23833  uzrest  23937  qustgpopn  24160  qustgplem  24161  cphsqrtcl  25226  lhop  26058  ig1peu  26215  ig1pdvds  26220  plypf1  26252  nosupno  27744  nosupbday  27746  noinfno  27759  noinfbday  27761  noetasuplem4  27777  noetainflem4  27781  eqcuts2  27856  cutsun12  27860  cutbdaybnd  27865  cutbdaybnd2  27866  cutbdaylt  27868  madebdaylemlrcut  27969  sltsbday  27987  cofcut1  27990  cofcutr  27994  lrrecfr  28013  negsproplem4  28101  negsproplem5  28102  negsproplem6  28103  f1otrg  29017  txomap  34092  sitgaddlemb  34606  f1resrcmplf1dlem  35344  noinfepfnregs  35392  cvmopnlem  35592  mrsubrn  35827  msubrn  35843  ttcid  36816  dfttc2g  36830  regsfromunir1  36864  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem23  38106  cnambfre  38131  ftc1anclem7  38162  ftc1anc  38164  aks6d1c2  42711  aks6d1c7lem1  42761  isnumbasgrplem1  43642  relpmin  45492  relpfrlem  45493  permaxun  45551  funimaeq  45785