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

Metamath Proof Explorer

Theorem suppssr

Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppssr.f 
|- ( ph -> F : A --> B )
suppssr.n 
|- ( ph -> ( F supp Z ) C_ W )
suppssr.a 
|- ( ph -> A e. V )
suppssr.z 
|- ( ph -> Z e. U )
Assertion suppssr 
|- ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )

Proof

Step Hyp Ref Expression
1 suppssr.f 
 |-  ( ph -> F : A --> B )
2 suppssr.n 
 |-  ( ph -> ( F supp Z ) C_ W )
3 suppssr.a 
 |-  ( ph -> A e. V )
4 suppssr.z 
 |-  ( ph -> Z e. U )
5 eldif 
 |-  ( X e. ( A \ W ) <-> ( X e. A /\ -. X e. W ) )
6 fvex 
 |-  ( F ` X ) e. _V
7 eldifsn 
 |-  ( ( F ` X ) e. ( _V \ { Z } ) <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) )
8 6 7 mpbiran 
 |-  ( ( F ` X ) e. ( _V \ { Z } ) <-> ( F ` X ) =/= Z )
9 1 ffnd 
 |-  ( ph -> F Fn A )
10 elsuppfn 
 |-  ( ( F Fn A /\ A e. V /\ Z e. U ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
11 9 3 4 10 syl3anc 
 |-  ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
12 ibar 
 |-  ( ( F ` X ) e. _V -> ( ( F ` X ) =/= Z <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) ) )
13 6 12 mp1i 
 |-  ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z <-> ( ( F ` X ) e. _V /\ ( F ` X ) =/= Z ) ) )
14 13 7 bitr4di 
 |-  ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z <-> ( F ` X ) e. ( _V \ { Z } ) ) )
15 14 pm5.32da 
 |-  ( ph -> ( ( X e. A /\ ( F ` X ) =/= Z ) <-> ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) ) )
16 11 15 bitrd 
 |-  ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) ) )
17 2 sseld 
 |-  ( ph -> ( X e. ( F supp Z ) -> X e. W ) )
18 16 17 sylbird 
 |-  ( ph -> ( ( X e. A /\ ( F ` X ) e. ( _V \ { Z } ) ) -> X e. W ) )
19 18 expdimp 
 |-  ( ( ph /\ X e. A ) -> ( ( F ` X ) e. ( _V \ { Z } ) -> X e. W ) )
20 8 19 biimtrrid 
 |-  ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z -> X e. W ) )
21 20 necon1bd 
 |-  ( ( ph /\ X e. A ) -> ( -. X e. W -> ( F ` X ) = Z ) )
22 21 impr 
 |-  ( ( ph /\ ( X e. A /\ -. X e. W ) ) -> ( F ` X ) = Z )
23 5 22 sylan2b 
 |-  ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )