Theorem fnfvima 7173

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898  dom cdm 5619   “ cima 5622  Fun wfun 6480   Fn wfn 6481  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-fv 6494

This theorem is referenced by:  fnfvimad  7174  isomin  7277  isofrlem  7280  fnwelem  8067  fimaproj  8071  php3  9125  fissuni  9248  unxpwdom2  9481  cantnflt  9569  dfac12lem2  10043  ackbij2  10140  isf34lem7  10277  isf34lem6  10278  zorn2lem2  10395  ttukeylem5  10411  tskuni  10681  axpre-sup  11067  limsupval2  15389  mgmhmima  18625  mhmimalem  18734  mhmima  18735  ghmnsgima  19154  psgnunilem1  19407  dprdfeq0  19938  dprd2dlem1  19957  rhmimasubrnglem  20482  lmhmima  20983  lmcnp  23220  basqtop  23627  tgqtop  23628  kqfvima  23646  reghmph  23709  uzrest  23813  qustgpopn  24036  qustgplem  24037  cphsqrtcl  25112  lhop  25949  ig1peu  26108  ig1pdvds  26113  plypf1  26145  nosupno  27643  nosupbday  27645  noinfno  27658  noinfbday  27660  noetasuplem4  27676  noetainflem4  27680  eqscut2  27748  scutun12  27752  scutbdaybnd  27757  scutbdaybnd2  27758  scutbdaylt  27760  madebdaylemlrcut  27845  cofcut1  27865  cofcutr  27869  lrrecfr  27887  negsproplem4  27974  negsproplem5  27975  negsproplem6  27976  f1otrg  28850  txomap  33868  sitgaddlemb  34382  f1resrcmplf1dlem  35119  cvmopnlem  35343  mrsubrn  35578  msubrn  35594  poimirlem4  37684  poimirlem6  37686  poimirlem7  37687  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem23  37703  cnambfre  37728  ftc1anclem7  37759  ftc1anc  37761  aks6d1c2  42243  aks6d1c7lem1  42293  isnumbasgrplem1  43218  relpmin  45069  relpfrlem  45070  permaxun  45128  funimaeq  45367