Theorem fnfvima 7235

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 6636	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1151	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1155	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6639	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1151	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3971	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 521	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1156	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7233	. 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 2145   ⊆ wss 3902  dom cdm 5659   “ cima 5662  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  fnfvimad  7236  f1resrcmplf1dlem  7274  isomin  7341  isofrlem  7344  fnwelem  8132  fimaproj  8136  php3  9206  fissuni  9327  unxpwdom2  9563  cantnflt  9654  dfac12lem2  10150  ackbij2  10247  isf34lem7  10384  isf34lem6  10385  zorn2lem2  10502  ttukeylem5  10518  tskuni  10795  axpre-sup  11181  limsupval2  15569  mgmhmima  18819  mhmimalem  18934  mhmima  18935  ghmnsgima  19368  psgnunilem1  19621  dprdfeq0  20152  dprd2dlem1  20171  rhmimasubrnglem  20728  lmhmima  21232  lmcnp  23530  basqtop  23938  tgqtop  23939  kqfvima  23957  reghmph  24020  uzrest  24124  qustgpopn  24347  qustgplem  24348  cphsqrtcl  25413  lhop  26245  ig1peu  26402  ig1pdvds  26407  plypf1  26439  nosupno  27937  nosupbday  27939  noinfno  27952  noinfbday  27954  noetasuplem4  27970  noetainflem4  27974  eqcuts2  28049  cutsun12  28053  cutbdaybnd  28058  cutbdaybnd2  28059  cutbdaylt  28061  madebdaylemlrcut  28162  sltsbday  28180  cofcut1  28183  cofcutr  28187  lrrecfr  28206  negsproplem4  28294  negsproplem5  28295  negsproplem6  28296  f1otrg  29313  txomap  34331  sitgaddlemb  34846  fnfvintima  35578  dfscott3  35613  noinfepfnregs  35645  cvmopnlem  35844  mrsubrn  36079  msubrn  36095  ttcid  37098  dfttc2g  37112  regsfromunir1  37146  poimirlem4  38360  poimirlem6  38362  poimirlem7  38363  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem23  38379  cnambfre  38404  ftc1anclem7  38435  ftc1anc  38437  aks6d1c2  42983  aks6d1c7lem1  43033  isnumbasgrplem1  43929  relpmin  45762  relpfrlem  45763  permaxun  45821  funimaeq  46062