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

Metamath Proof Explorer

Theorem funimassd

Description: Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 funimassd.1 
 |-  F/ x ph
2 funimassd.2 
 |-  ( ph -> Fun F )
3 funimassd.3 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
4 fvelima 
 |-  ( ( Fun F /\ y e. ( F " A ) ) -> E. x e. A ( F ` x ) = y )
5 2 4 sylan 
 |-  ( ( ph /\ y e. ( F " A ) ) -> E. x e. A ( F ` x ) = y )
6 nfv 
 |-  F/ x y e. ( F " A )
7 1 6 nfan 
 |-  F/ x ( ph /\ y e. ( F " A ) )
8 nfv 
 |-  F/ x y e. B
9 id 
 |-  ( ( F ` x ) = y -> ( F ` x ) = y )
10 9 eqcomd 
 |-  ( ( F ` x ) = y -> y = ( F ` x ) )
11 10 3ad2ant3 
 |-  ( ( ph /\ x e. A /\ ( F ` x ) = y ) -> y = ( F ` x ) )
12 3 3adant3 
 |-  ( ( ph /\ x e. A /\ ( F ` x ) = y ) -> ( F ` x ) e. B )
13 11 12 eqeltrd 
 |-  ( ( ph /\ x e. A /\ ( F ` x ) = y ) -> y e. B )
14 13 3exp 
 |-  ( ph -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
15 14 adantr 
 |-  ( ( ph /\ y e. ( F " A ) ) -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
16 7 8 15 rexlimd 
 |-  ( ( ph /\ y e. ( F " A ) ) -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
17 5 16 mpd 
 |-  ( ( ph /\ y e. ( F " A ) ) -> y e. B )
18 17 ex 
 |-  ( ph -> ( y e. ( F " A ) -> y e. B ) )
19 18 ssrdv 
 |-  ( ph -> ( F " A ) C_ B )