Metamath Proof Explorer


Theorem suppss2f

Description: Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017) (Revised by AV, 1-Sep-2020)

Ref Expression
Hypotheses suppss2f.p kφ
suppss2f.a _kA
suppss2f.w _kW
suppss2f.n φkAWB=Z
suppss2f.v φAV
Assertion suppss2f φkABsuppZW

Proof

Step Hyp Ref Expression
1 suppss2f.p kφ
2 suppss2f.a _kA
3 suppss2f.w _kW
4 suppss2f.n φkAWB=Z
5 suppss2f.v φAV
6 nfcv _lA
7 nfcv _lB
8 nfcsb1v _kl/kB
9 csbeq1a k=lB=l/kB
10 2 6 7 8 9 cbvmptf kAB=lAl/kB
11 10 oveq1i kABsuppZ=lAl/kBsuppZ
12 4 sbt lkφkAWB=Z
13 sbim lkφkAWB=ZlkφkAWlkB=Z
14 sban lkφkAWlkφlkkAW
15 1 sbf lkφφ
16 2 3 nfdif _kAW
17 16 clelsb1fw lkkAWlAW
18 15 17 anbi12i lkφlkkAWφlAW
19 14 18 bitri lkφkAWφlAW
20 sbsbc lkB=Z[˙l/k]˙B=Z
21 sbceq1g lV[˙l/k]˙B=Zl/kB=Z
22 21 elv [˙l/k]˙B=Zl/kB=Z
23 20 22 bitri lkB=Zl/kB=Z
24 19 23 imbi12i lkφkAWlkB=ZφlAWl/kB=Z
25 13 24 bitri lkφkAWB=ZφlAWl/kB=Z
26 12 25 mpbi φlAWl/kB=Z
27 26 5 suppss2 φlAl/kBsuppZW
28 11 27 eqsstrid φkABsuppZW