Metamath Proof Explorer

Theorem funimass4f

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017)

Ref Expression
Hypotheses funimass4f.1 
|- F/_ x A
funimass4f.2 
|- F/_ x B
funimass4f.3 
|- F/_ x F
Assertion funimass4f 
|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 funimass4f.1 
 |-  F/_ x A
2 funimass4f.2 
 |-  F/_ x B
3 funimass4f.3 
 |-  F/_ x F
4 3 nffun 
 |-  F/ x Fun F
5 3 nfdm 
 |-  F/_ x dom F
6 1 5 nfss 
 |-  F/ x A C_ dom F
7 4 6 nfan 
 |-  F/ x ( Fun F /\ A C_ dom F )
8 3 1 nfima 
 |-  F/_ x ( F " A )
9 8 2 nfss 
 |-  F/ x ( F " A ) C_ B
10 7 9 nfan 
 |-  F/ x ( ( Fun F /\ A C_ dom F ) /\ ( F " A ) C_ B )
11 funfvima2 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( x e. A -> ( F ` x ) e. ( F " A ) ) )
12 ssel 
 |-  ( ( F " A ) C_ B -> ( ( F ` x ) e. ( F " A ) -> ( F ` x ) e. B ) )
13 11 12 sylan9 
 |-  ( ( ( Fun F /\ A C_ dom F ) /\ ( F " A ) C_ B ) -> ( x e. A -> ( F ` x ) e. B ) )
14 10 13 ralrimi 
 |-  ( ( ( Fun F /\ A C_ dom F ) /\ ( F " A ) C_ B ) -> A. x e. A ( F ` x ) e. B )
15 1 3 dfimafnf 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A y = ( F ` x ) } )
16 15 adantr 
 |-  ( ( ( Fun F /\ A C_ dom F ) /\ A. x e. A ( F ` x ) e. B ) -> ( F " A ) = { y | E. x e. A y = ( F ` x ) } )
17 2 abrexss 
 |-  ( A. x e. A ( F ` x ) e. B -> { y | E. x e. A y = ( F ` x ) } C_ B )
18 17 adantl 
 |-  ( ( ( Fun F /\ A C_ dom F ) /\ A. x e. A ( F ` x ) e. B ) -> { y | E. x e. A y = ( F ` x ) } C_ B )
19 16 18 eqsstrd 
 |-  ( ( ( Fun F /\ A C_ dom F ) /\ A. x e. A ( F ` x ) e. B ) -> ( F " A ) C_ B )
20 14 19 impbida 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A. x e. A ( F ` x ) e. B ) )