This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnfvima

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)

Ref Expression
Assertion fnfvima 
|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " S ) )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( F Fn A -> Fun F )
2 1 3ad2ant1 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> Fun F )
3 simp2 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> S C_ A )
4 fndm 
 |-  ( F Fn A -> dom F = A )
5 4 3ad2ant1 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> dom F = A )
6 3 5 sseqtrrd 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> S C_ dom F )
7 2 6 jca 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( Fun F /\ S C_ dom F ) )
8 simp3 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> X e. S )
9 funfvima2 
 |-  ( ( Fun F /\ S C_ dom F ) -> ( X e. S -> ( F ` X ) e. ( F " S ) ) )
10 7 8 9 sylc 
 |-  ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " S ) )