Theorem fnfvima 7188

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 6598	. . . 4 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹)
2	1	3ad2ant1 1134	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → Fun 𝐹)
3		simp2 1138	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ 𝐴)
4		fndm 6601	. . . . 5 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
5	4	3ad2ant1 1134	. . . 4 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → dom 𝐹 = 𝐴)
6	3, 5	sseqtrrd 3959	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑆 ⊆ dom 𝐹)
7	2, 6	jca 511	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹))
8		simp3 1139	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ 𝑆)
9		funfvima2 7186	. 2 ⊢ ((Fun 𝐹 ∧ 𝑆 ⊆ dom 𝐹) → (𝑋 ∈ 𝑆 → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆)))
10	7, 8, 9	sylc 65	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (𝐹‘𝑋) ∈ (𝐹 “ 𝑆))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889  dom cdm 5631   “ cima 5634  Fun wfun 6492   Fn wfn 6493  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  fnfvimad  7189  isomin  7292  isofrlem  7295  fnwelem  8081  fimaproj  8085  php3  9143  fissuni  9267  unxpwdom2  9503  cantnflt  9593  dfac12lem2  10067  ackbij2  10164  isf34lem7  10301  isf34lem6  10302  zorn2lem2  10419  ttukeylem5  10435  tskuni  10706  axpre-sup  11092  limsupval2  15442  mgmhmima  18683  mhmimalem  18792  mhmima  18793  ghmnsgima  19215  psgnunilem1  19468  dprdfeq0  19999  dprd2dlem1  20018  rhmimasubrnglem  20542  lmhmima  21042  lmcnp  23269  basqtop  23676  tgqtop  23677  kqfvima  23695  reghmph  23758  uzrest  23862  qustgpopn  24085  qustgplem  24086  cphsqrtcl  25151  lhop  25983  ig1peu  26140  ig1pdvds  26145  plypf1  26177  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  noetasuplem4  27700  noetainflem4  27704  eqcuts2  27778  cutsun12  27782  cutbdaybnd  27787  cutbdaybnd2  27788  cutbdaylt  27790  madebdaylemlrcut  27891  sltsbday  27909  cofcut1  27912  cofcutr  27916  lrrecfr  27935  negsproplem4  28023  negsproplem5  28024  negsproplem6  28025  f1otrg  28939  txomap  33978  sitgaddlemb  34492  f1resrcmplf1dlem  35229  noinfepfnregs  35276  cvmopnlem  35460  mrsubrn  35695  msubrn  35711  ttcid  36674  dfttc2g  36688  regsfromunir1  36722  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  cnambfre  37989  ftc1anclem7  38020  ftc1anc  38022  aks6d1c2  42569  aks6d1c7lem1  42619  isnumbasgrplem1  43529  relpmin  45379  relpfrlem  45380  permaxun  45438  funimaeq  45675