Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnfvima Structured version   Visualization version   GIF version

Theorem fnfvima 6983
 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
StepHypRef Expression
1 fnfun 6431 . . . 4 (𝐹 Fn 𝐴 → Fun 𝐹)
213ad2ant1 1130 . . 3 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → Fun 𝐹)
3 simp2 1134 . . . 4 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → 𝑆𝐴)
4 fndm 6433 . . . . 5 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
543ad2ant1 1130 . . . 4 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → dom 𝐹 = 𝐴)
63, 5sseqtrrd 3958 . . 3 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → 𝑆 ⊆ dom 𝐹)
72, 6jca 515 . 2 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → (Fun 𝐹𝑆 ⊆ dom 𝐹))
8 simp3 1135 . 2 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → 𝑋𝑆)
9 funfvima2 6981 . 2 ((Fun 𝐹𝑆 ⊆ dom 𝐹) → (𝑋𝑆 → (𝐹𝑋) ∈ (𝐹𝑆)))
107, 8, 9sylc 65 1 ((𝐹 Fn 𝐴𝑆𝐴𝑋𝑆) → (𝐹𝑋) ∈ (𝐹𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ⊆ wss 3883  dom cdm 5523   “ cima 5526  Fun wfun 6326   Fn wfn 6327  ‘cfv 6332 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-fv 6340 This theorem is referenced by:  fnfvimad  6984  isomin  7079  isofrlem  7082  fnwelem  7821  fimaproj  7825  php3  8705  fissuni  8831  unxpwdom2  9054  cantnflt  9137  dfac12lem2  9573  ackbij2  9672  isf34lem7  9808  isf34lem6  9809  zorn2lem2  9926  ttukeylem5  9942  tskuni  10212  axpre-sup  10598  limsupval2  14849  mhmima  18001  ghmnsgima  18395  psgnunilem1  18634  dprdfeq0  19158  dprd2dlem1  19177  lmhmima  19833  lmcnp  21950  basqtop  22357  tgqtop  22358  kqfvima  22376  reghmph  22439  uzrest  22543  qustgpopn  22766  qustgplem  22767  cphsqrtcl  23830  lhop  24660  ig1peu  24816  ig1pdvds  24821  plypf1  24853  f1otrg  26709  txomap  31253  sitgaddlemb  31782  f1resrcmplf1dlem  32535  cvmopnlem  32704  mrsubrn  32939  msubrn  32955  nosupno  33393  nosupbday  33395  noinfno  33408  noinfbday  33410  noetasuplem4  33426  noetainflem4  33430  eqscut2  33482  scutun12  33486  scutbdaybnd  33491  scutbdaybnd2  33492  scutbdaylt  33494  poimirlem4  35212  poimirlem6  35214  poimirlem7  35215  poimirlem16  35224  poimirlem17  35225  poimirlem19  35227  poimirlem20  35228  poimirlem23  35231  cnambfre  35256  ftc1anclem7  35287  ftc1anc  35289  isnumbasgrplem1  40216  funimaeq  42052  mgmhmima  44590
 Copyright terms: Public domain W3C validator