Theorem fnfvima 7225

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  dom cdm 5654   “ cima 5657  Fun wfun 6525   Fn wfn 6526  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is referenced by:  fnfvimad  7226  isomin  7330  isofrlem  7333  fnwelem  8130  fimaproj  8134  php3  9223  php3OLD  9233  fissuni  9369  unxpwdom2  9602  cantnflt  9686  dfac12lem2  10159  ackbij2  10256  isf34lem7  10393  isf34lem6  10394  zorn2lem2  10511  ttukeylem5  10527  tskuni  10797  axpre-sup  11183  limsupval2  15496  mgmhmima  18693  mhmimalem  18802  mhmima  18803  ghmnsgima  19223  psgnunilem1  19474  dprdfeq0  20005  dprd2dlem1  20024  rhmimasubrnglem  20525  lmhmima  21005  lmcnp  23242  basqtop  23649  tgqtop  23650  kqfvima  23668  reghmph  23731  uzrest  23835  qustgpopn  24058  qustgplem  24059  cphsqrtcl  25136  lhop  25973  ig1peu  26132  ig1pdvds  26137  plypf1  26169  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  noetasuplem4  27700  noetainflem4  27704  eqscut2  27770  scutun12  27774  scutbdaybnd  27779  scutbdaybnd2  27780  scutbdaylt  27782  madebdaylemlrcut  27862  cofcut1  27880  cofcutr  27884  lrrecfr  27902  negsproplem4  27989  negsproplem5  27990  negsproplem6  27991  f1otrg  28850  txomap  33865  sitgaddlemb  34380  f1resrcmplf1dlem  35117  cvmopnlem  35300  mrsubrn  35535  msubrn  35551  poimirlem4  37648  poimirlem6  37650  poimirlem7  37651  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  poimirlem23  37667  cnambfre  37692  ftc1anclem7  37723  ftc1anc  37725  aks6d1c2  42143  aks6d1c7lem1  42193  isnumbasgrplem1  43125  relpmin  44977  relpfrlem  44978  permaxun  45036  funimaeq  45270