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 )