Theorem fnfvima 7236

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 6648	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1131	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1135	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6651	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1131	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 4022	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 510	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1136	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7234	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   ⊆ wss 3947  dom cdm 5675   “ cima 5678  Fun wfun 6536   Fn wfn 6537  ‘cfv 6542

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550

This theorem is referenced by:  fnfvimad  7237  isomin  7336  isofrlem  7339  fnwelem  8119  fimaproj  8123  php3  9214  php3OLD  9226  fissuni  9359  unxpwdom2  9585  cantnflt  9669  dfac12lem2  10141  ackbij2  10240  isf34lem7  10376  isf34lem6  10377  zorn2lem2  10494  ttukeylem5  10510  tskuni  10780  axpre-sup  11166  limsupval2  15428  mgmhmima  18640  mhmimalem  18741  mhmima  18742  ghmnsgima  19154  psgnunilem1  19402  dprdfeq0  19933  dprd2dlem1  19952  rhmimasubrnglem  20453  lmhmima  20802  lmcnp  23028  basqtop  23435  tgqtop  23436  kqfvima  23454  reghmph  23517  uzrest  23621  qustgpopn  23844  qustgplem  23845  cphsqrtcl  24932  lhop  25768  ig1peu  25924  ig1pdvds  25929  plypf1  25961  nosupno  27442  nosupbday  27444  noinfno  27457  noinfbday  27459  noetasuplem4  27475  noetainflem4  27479  eqscut2  27544  scutun12  27548  scutbdaybnd  27553  scutbdaybnd2  27554  scutbdaylt  27556  madebdaylemlrcut  27630  cofcut1  27645  cofcutr  27649  lrrecfr  27665  negsproplem4  27744  negsproplem5  27745  negsproplem6  27746  f1otrg  28389  txomap  33112  sitgaddlemb  33645  f1resrcmplf1dlem  34387  cvmopnlem  34567  mrsubrn  34802  msubrn  34818  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem23  36814  cnambfre  36839  ftc1anclem7  36870  ftc1anc  36872  isnumbasgrplem1  42145  funimaeq  44248