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

Metamath Proof Explorer

Theorem suppssrg

Description: A function is zero outside its support. Version of suppssr avoiding ax-rep by assuming F is a set rather than its domain A . (Contributed by SN, 5-May-2024)

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

Proof

Step Hyp Ref Expression
1 suppssrg.f 
 |-  ( ph -> F : A --> B )
2 suppssrg.n 
 |-  ( ph -> ( F supp Z ) C_ W )
3 suppssrg.a 
 |-  ( ph -> F e. V )
4 suppssrg.z 
 |-  ( ph -> Z e. U )
5 eldif 
 |-  ( X e. ( A \ W ) <-> ( X e. A /\ -. X e. W ) )
6 1 ffnd 
 |-  ( ph -> F Fn A )
7 elsuppfng 
 |-  ( ( F Fn A /\ F e. V /\ Z e. U ) -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
8 6 3 4 7 syl3anc 
 |-  ( ph -> ( X e. ( F supp Z ) <-> ( X e. A /\ ( F ` X ) =/= Z ) ) )
9 2 sseld 
 |-  ( ph -> ( X e. ( F supp Z ) -> X e. W ) )
10 8 9 sylbird 
 |-  ( ph -> ( ( X e. A /\ ( F ` X ) =/= Z ) -> X e. W ) )
11 10 expdimp 
 |-  ( ( ph /\ X e. A ) -> ( ( F ` X ) =/= Z -> X e. W ) )
12 11 necon1bd 
 |-  ( ( ph /\ X e. A ) -> ( -. X e. W -> ( F ` X ) = Z ) )
13 12 impr 
 |-  ( ( ph /\ ( X e. A /\ -. X e. W ) ) -> ( F ` X ) = Z )
14 5 13 sylan2b 
 |-  ( ( ph /\ X e. ( A \ W ) ) -> ( F ` X ) = Z )