# 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 ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to {F}\left({X}\right)\in {F}\left[{S}\right]$

### Proof

Step Hyp Ref Expression
1 fnfun ${⊢}{F}Fn{A}\to \mathrm{Fun}{F}$
2 1 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to \mathrm{Fun}{F}$
3 simp2 ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to {S}\subseteq {A}$
4 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
5 4 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to \mathrm{dom}{F}={A}$
6 3 5 sseqtrrd ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to {S}\subseteq \mathrm{dom}{F}$
7 2 6 jca ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to \left(\mathrm{Fun}{F}\wedge {S}\subseteq \mathrm{dom}{F}\right)$
8 simp3 ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to {X}\in {S}$
9 funfvima2 ${⊢}\left(\mathrm{Fun}{F}\wedge {S}\subseteq \mathrm{dom}{F}\right)\to \left({X}\in {S}\to {F}\left({X}\right)\in {F}\left[{S}\right]\right)$
10 7 8 9 sylc ${⊢}\left({F}Fn{A}\wedge {S}\subseteq {A}\wedge {X}\in {S}\right)\to {F}\left({X}\right)\in {F}\left[{S}\right]$