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

Metamath Proof Explorer

Theorem suppss

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019) (Proof shortened by SN, 5-Aug-2024)

Ref Expression
Hypotheses suppss.f 
|- ( ph -> F : A --> B )
suppss.n 
|- ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
Assertion suppss 
|- ( ph -> ( F supp Z ) C_ W )

Proof

Step Hyp Ref Expression
1 suppss.f 
 |-  ( ph -> F : A --> B )
2 suppss.n 
 |-  ( ( ph /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
3 1 ffnd 
 |-  ( ph -> F Fn A )
4 3 adantl 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> F Fn A )
5 simpll 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> F e. _V )
6 simplr 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )
7 elsuppfng 
 |-  ( ( F Fn A /\ F e. _V /\ Z e. _V ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
8 4 5 6 7 syl3anc 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
9 eldif 
 |-  ( k e. ( A \ W ) <-> ( k e. A /\ -. k e. W ) )
10 2 adantll 
 |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. ( A \ W ) ) -> ( F ` k ) = Z )
11 9 10 sylan2br 
 |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ ( k e. A /\ -. k e. W ) ) -> ( F ` k ) = Z )
12 11 expr 
 |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( -. k e. W -> ( F ` k ) = Z ) )
13 12 necon1ad 
 |-  ( ( ( ( F e. _V /\ Z e. _V ) /\ ph ) /\ k e. A ) -> ( ( F ` k ) =/= Z -> k e. W ) )
14 13 expimpd 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( ( k e. A /\ ( F ` k ) =/= Z ) -> k e. W ) )
15 8 14 sylbid 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( k e. ( F supp Z ) -> k e. W ) )
16 15 ssrdv 
 |-  ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) C_ W )
17 16 ex 
 |-  ( ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )
18 supp0prc 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
19 0ss 
 |-  (/) C_ W
20 18 19 eqsstrdi 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ W )
21 20 a1d 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ W ) )
22 17 21 pm2.61i 
 |-  ( ph -> ( F supp Z ) C_ W )