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 
|- F/ k ph
suppss2f.a 
|- F/_ k A
suppss2f.w 
|- F/_ k W
suppss2f.n 
|- ( ( ph /\ k e. ( A \ W ) ) -> B = Z )
suppss2f.v 
|- ( ph -> A e. V )
Assertion suppss2f 
|- ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W )

Proof

Step Hyp Ref Expression
1 suppss2f.p 
 |-  F/ k ph
2 suppss2f.a 
 |-  F/_ k A
3 suppss2f.w 
 |-  F/_ k W
4 suppss2f.n 
 |-  ( ( ph /\ k e. ( A \ W ) ) -> B = Z )
5 suppss2f.v 
 |-  ( ph -> A e. V )
6 nfcv 
 |-  F/_ l A
7 nfcv 
 |-  F/_ l B
8 nfcsb1v 
 |-  F/_ k [_ l / k ]_ B
9 csbeq1a 
 |-  ( k = l -> B = [_ l / k ]_ B )
10 2 6 7 8 9 cbvmptf 
 |-  ( k e. A |-> B ) = ( l e. A |-> [_ l / k ]_ B )
11 10 oveq1i 
 |-  ( ( k e. A |-> B ) supp Z ) = ( ( l e. A |-> [_ l / k ]_ B ) supp Z )
12 4 sbt 
 |-  [ l / k ] ( ( ph /\ k e. ( A \ W ) ) -> B = Z )
13 sbim 
 |-  ( [ l / k ] ( ( ph /\ k e. ( A \ W ) ) -> B = Z ) <-> ( [ l / k ] ( ph /\ k e. ( A \ W ) ) -> [ l / k ] B = Z ) )
14 sban 
 |-  ( [ l / k ] ( ph /\ k e. ( A \ W ) ) <-> ( [ l / k ] ph /\ [ l / k ] k e. ( A \ W ) ) )
15 1 sbf 
 |-  ( [ l / k ] ph <-> ph )
16 2 3 nfdif 
 |-  F/_ k ( A \ W )
17 16 clelsb3fw 
 |-  ( [ l / k ] k e. ( A \ W ) <-> l e. ( A \ W ) )
18 15 17 anbi12i 
 |-  ( ( [ l / k ] ph /\ [ l / k ] k e. ( A \ W ) ) <-> ( ph /\ l e. ( A \ W ) ) )
19 14 18 bitri 
 |-  ( [ l / k ] ( ph /\ k e. ( A \ W ) ) <-> ( ph /\ l e. ( A \ W ) ) )
20 sbsbc 
 |-  ( [ l / k ] B = Z <-> [. l / k ]. B = Z )
21 sbceq1g 
 |-  ( l e. _V -> ( [. l / k ]. B = Z <-> [_ l / k ]_ B = Z ) )
22 21 elv 
 |-  ( [. l / k ]. B = Z <-> [_ l / k ]_ B = Z )
23 20 22 bitri 
 |-  ( [ l / k ] B = Z <-> [_ l / k ]_ B = Z )
24 19 23 imbi12i 
 |-  ( ( [ l / k ] ( ph /\ k e. ( A \ W ) ) -> [ l / k ] B = Z ) <-> ( ( ph /\ l e. ( A \ W ) ) -> [_ l / k ]_ B = Z ) )
25 13 24 bitri 
 |-  ( [ l / k ] ( ( ph /\ k e. ( A \ W ) ) -> B = Z ) <-> ( ( ph /\ l e. ( A \ W ) ) -> [_ l / k ]_ B = Z ) )
26 12 25 mpbi 
 |-  ( ( ph /\ l e. ( A \ W ) ) -> [_ l / k ]_ B = Z )
27 26 5 suppss2 
 |-  ( ph -> ( ( l e. A |-> [_ l / k ]_ B ) supp Z ) C_ W )
28 11 27 eqsstrid 
 |-  ( ph -> ( ( k e. A |-> B ) supp Z ) C_ W )