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 φF:AB
suppssr.n φFsuppZW
suppssr.a φAV
suppssr.z φZU
Assertion suppssr φXAWFX=Z

Proof

Step Hyp Ref Expression
1 suppssr.f φF:AB
2 suppssr.n φFsuppZW
3 suppssr.a φAV
4 suppssr.z φZU
5 eldif XAWXA¬XW
6 fvex FXV
7 eldifsn FXVZFXVFXZ
8 6 7 mpbiran FXVZFXZ
9 1 ffnd φFFnA
10 elsuppfn FFnAAVZUXsuppZFXAFXZ
11 9 3 4 10 syl3anc φXsuppZFXAFXZ
12 ibar FXVFXZFXVFXZ
13 6 12 mp1i φXAFXZFXVFXZ
14 13 7 bitr4di φXAFXZFXVZ
15 14 pm5.32da φXAFXZXAFXVZ
16 11 15 bitrd φXsuppZFXAFXVZ
17 2 sseld φXsuppZFXW
18 16 17 sylbird φXAFXVZXW
19 18 expdimp φXAFXVZXW
20 8 19 syl5bir φXAFXZXW
21 20 necon1bd φXA¬XWFX=Z
22 21 impr φXA¬XWFX=Z
23 5 22 sylan2b φXAWFX=Z