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

Theorem fnfvima 5842
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  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  ( F `  X )  e.  ( F " S
) )

Proof of Theorem fnfvima
StepHypRef Expression
1 fnfun 5423 . . . 4  |-  ( F  Fn  A  ->  Fun  F )
213ad2ant1 976 . . 3  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  Fun  F )
3 simp2 956 . . . 4  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  S  C_  A )
4 fndm 5425 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
543ad2ant1 976 . . . 4  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  dom  F  =  A )
63, 5sseqtr4d 3291 . . 3  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  S  C_ 
dom  F )
72, 6jca 518 . 2  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  ( Fun  F  /\  S  C_  dom  F ) )
8 simp3 957 . 2  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  X  e.  S )
9 funfvima2 5840 . 2  |-  ( ( Fun  F  /\  S  C_ 
dom  F )  -> 
( X  e.  S  ->  ( F `  X
)  e.  ( F
" S ) ) )
107, 8, 9sylc 56 1  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  ( F `  X )  e.  ( F " S
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1642    e. wcel 1710    C_ wss 3228   dom cdm 4771   "cima 4774   Fun wfun 5331    Fn wfn 5332   ` cfv 5337
This theorem is referenced by:  isomin  5921  isofrlem  5924  fnwelem  6317  php3  7135  fissuni  7250  unxpwdom2  7392  cantnflt  7463  mapfien  7489  dfac12lem2  7860  ackbij2  7959  isf34lem7  8095  isf34lem6  8096  zorn2lem2  8214  ttukeylem5  8230  tskuni  8495  axpre-sup  8881  limsupval2  12050  mhmima  14539  ghmnsgima  14805  dprdfeq0  15356  dprd2dlem1  15375  lmhmima  15903  lmcnp  17138  basqtop  17508  tgqtop  17509  kqfvima  17527  reghmph  17590  uzrest  17694  divstgpopn  17904  divstgplem  17905  cphsqrcl  18724  lhop  19467  ig1peu  19661  ig1pdvds  19666  plypf1  19698  cvmopnlem  24213  nobndlem8  24911  isnumbasgrplem1  26589  psgnunilem1  26739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-fv 5345
  Copyright terms: Public domain W3C validator