Theorem fnfvima 7184

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 6592	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1139	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1143	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6595	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1139	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3959	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 516	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1144	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7182	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890  dom cdm 5625   “ cima 5628  Fun wfun 6486   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  fnfvimad  7185  isomin  7288  isofrlem  7291  fnwelem  8078  fimaproj  8082  php3  9140  fissuni  9264  unxpwdom2  9500  cantnflt  9591  dfac12lem2  10065  ackbij2  10162  isf34lem7  10299  isf34lem6  10300  zorn2lem2  10417  ttukeylem5  10433  tskuni  10704  axpre-sup  11090  limsupval2  15440  mgmhmima  18681  mhmimalem  18790  mhmima  18791  ghmnsgima  19213  psgnunilem1  19466  dprdfeq0  19997  dprd2dlem1  20016  rhmimasubrnglem  20544  lmhmima  21044  lmcnp  23294  basqtop  23701  tgqtop  23702  kqfvima  23720  reghmph  23783  uzrest  23887  qustgpopn  24110  qustgplem  24111  cphsqrtcl  25176  lhop  26008  ig1peu  26165  ig1pdvds  26170  plypf1  26202  nosupno  27692  nosupbday  27694  noinfno  27707  noinfbday  27709  noetasuplem4  27725  noetainflem4  27729  eqcuts2  27803  cutsun12  27807  cutbdaybnd  27812  cutbdaybnd2  27813  cutbdaylt  27815  madebdaylemlrcut  27916  sltsbday  27934  cofcut1  27937  cofcutr  27941  lrrecfr  27960  negsproplem4  28048  negsproplem5  28049  negsproplem6  28050  f1otrg  28964  txomap  34025  sitgaddlemb  34539  f1resrcmplf1dlem  35274  noinfepfnregs  35320  cvmopnlem  35513  mrsubrn  35748  msubrn  35764  ttcid  36727  dfttc2g  36741  regsfromunir1  36775  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem23  38017  cnambfre  38042  ftc1anclem7  38073  ftc1anc  38075  aks6d1c2  42622  aks6d1c7lem1  42672  isnumbasgrplem1  43553  relpmin  45403  relpfrlem  45404  permaxun  45462  funimaeq  45697