Theorem fnfvima 7207

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914  dom cdm 5638   “ cima 5641  Fun wfun 6505   Fn wfn 6506  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  fnfvimad  7208  isomin  7312  isofrlem  7315  fnwelem  8110  fimaproj  8114  php3  9173  fissuni  9308  unxpwdom2  9541  cantnflt  9625  dfac12lem2  10098  ackbij2  10195  isf34lem7  10332  isf34lem6  10333  zorn2lem2  10450  ttukeylem5  10466  tskuni  10736  axpre-sup  11122  limsupval2  15446  mgmhmima  18642  mhmimalem  18751  mhmima  18752  ghmnsgima  19172  psgnunilem1  19423  dprdfeq0  19954  dprd2dlem1  19973  rhmimasubrnglem  20474  lmhmima  20954  lmcnp  23191  basqtop  23598  tgqtop  23599  kqfvima  23617  reghmph  23680  uzrest  23784  qustgpopn  24007  qustgplem  24008  cphsqrtcl  25084  lhop  25921  ig1peu  26080  ig1pdvds  26085  plypf1  26117  nosupno  27615  nosupbday  27617  noinfno  27630  noinfbday  27632  noetasuplem4  27648  noetainflem4  27652  eqscut2  27718  scutun12  27722  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  madebdaylemlrcut  27810  cofcut1  27828  cofcutr  27832  lrrecfr  27850  negsproplem4  27937  negsproplem5  27938  negsproplem6  27939  f1otrg  28798  txomap  33824  sitgaddlemb  34339  f1resrcmplf1dlem  35076  cvmopnlem  35265  mrsubrn  35500  msubrn  35516  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  cnambfre  37662  ftc1anclem7  37693  ftc1anc  37695  aks6d1c2  42118  aks6d1c7lem1  42168  isnumbasgrplem1  43090  relpmin  44942  relpfrlem  44943  permaxun  45001  funimaeq  45240