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

Theorem fnfvima 5942
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 5496 . . . 4  |-  ( F  Fn  A  ->  Fun  F )
213ad2ant1 1002 . . 3  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  Fun  F )
3 simp2 982 . . . 4  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  S  C_  A )
4 fndm 5498 . . . . 5  |-  ( F  Fn  A  ->  dom  F  =  A )
543ad2ant1 1002 . . . 4  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  dom  F  =  A )
63, 5sseqtr4d 3381 . . 3  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  S  C_ 
dom  F )
72, 6jca 529 . 2  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  ( Fun  F  /\  S  C_  dom  F ) )
8 simp3 983 . 2  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  X  e.  S )
9 funfvima2 5940 . 2  |-  ( ( Fun  F  /\  S  C_ 
dom  F )  -> 
( X  e.  S  ->  ( F `  X
)  e.  ( F
" S ) ) )
107, 8, 9sylc 60 1  |-  ( ( F  Fn  A  /\  S  C_  A  /\  X  e.  S )  ->  ( F `  X )  e.  ( F " S
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958    = wceq 1362    e. wcel 1755    C_ wss 3316   dom cdm 4827   "cima 4830   Fun wfun 5400    Fn wfn 5401   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-fv 5414
This theorem is referenced by:  isomin  6015  isofrlem  6018  fnwelem  6676  php3  7485  fissuni  7604  unxpwdom2  7791  cantnflt  7868  cantnfltOLD  7898  mapfienOLD  7915  dfac12lem2  8301  ackbij2  8400  isf34lem7  8536  isf34lem6  8537  zorn2lem2  8654  ttukeylem5  8670  tskuni  8938  axpre-sup  9324  limsupval2  12942  mhmima  15473  ghmnsgima  15750  psgnunilem1  15979  dprdfeq0  16486  dprdfeq0OLD  16493  dprd2dlem1  16514  lmhmima  17050  lmcnp  18750  basqtop  19126  tgqtop  19127  kqfvima  19145  reghmph  19208  uzrest  19312  divstgpopn  19532  divstgplem  19533  cphsqrcl  20545  lhop  21330  ig1peu  21528  ig1pdvds  21533  plypf1  21565  f1otrg  22940  cvmopnlem  27015  nobndlem8  27687  cnambfre  28284  ftc1anclem7  28317  ftc1anc  28319  isnumbasgrplem1  29302
  Copyright terms: Public domain W3C validator