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

Metamath Proof Explorer

Theorem fnfvimad

Description: A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses fnfvimad.1 
|- ( ph -> F Fn A )
fnfvimad.2 
|- ( ph -> B e. A )
fnfvimad.3 
|- ( ph -> B e. C )
Assertion fnfvimad 
|- ( ph -> ( F ` B ) e. ( F " C ) )

Proof

Step Hyp Ref Expression
1 fnfvimad.1 
 |-  ( ph -> F Fn A )
2 fnfvimad.2 
 |-  ( ph -> B e. A )
3 fnfvimad.3 
 |-  ( ph -> B e. C )
4 inss2 
 |-  ( A i^i C ) C_ C
5 imass2 
 |-  ( ( A i^i C ) C_ C -> ( F " ( A i^i C ) ) C_ ( F " C ) )
6 4 5 ax-mp 
 |-  ( F " ( A i^i C ) ) C_ ( F " C )
7 inss1 
 |-  ( A i^i C ) C_ A
8 7 a1i 
 |-  ( ph -> ( A i^i C ) C_ A )
9 2 3 elind 
 |-  ( ph -> B e. ( A i^i C ) )
10 fnfvima 
 |-  ( ( F Fn A /\ ( A i^i C ) C_ A /\ B e. ( A i^i C ) ) -> ( F ` B ) e. ( F " ( A i^i C ) ) )
11 1 8 9 10 syl3anc 
 |-  ( ph -> ( F ` B ) e. ( F " ( A i^i C ) ) )
12 6 11 sselid 
 |-  ( ph -> ( F ` B ) e. ( F " C ) )