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

Metamath Proof Explorer

Theorem suppgsumssiun

Description: The support of a function defined as a group sum is a subset of the indexed union of the supports. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses suppgsumssiun.1 ⊢ 𝑍 = ( 0g ‘ 𝑀 )
suppgsumssiun.2 ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
suppgsumssiun.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
suppgsumssiun.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
suppgsumssiun.5 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑋 )
Assertion suppgsumssiun ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) ) supp 𝑍 ) ⊆ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 suppgsumssiun.1 ⊢ 𝑍 = ( 0g ‘ 𝑀 )
2 suppgsumssiun.2 ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
3 suppgsumssiun.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 suppgsumssiun.4 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 suppgsumssiun.5 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑋 )
6 nfv ⊢ Ⅎ 𝑥 𝜑
7 nfcv ⊢ Ⅎ 𝑥 𝐴
8 nfcv ⊢ Ⅎ 𝑥 𝐵
9 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
10 nfcv ⊢ Ⅎ 𝑥 supp
11 nfcv ⊢ Ⅎ 𝑥 𝑍
12 9 10 11 nfov ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 )
13 8 12 nfiun ⊢ Ⅎ 𝑥 ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 )
14 mpt0 ⊢ ( 𝑦 ∈ ∅ ↦ 𝐶 ) = ∅
15 14 oveq2i ⊢ ( 𝑀 Σg ( 𝑦 ∈ ∅ ↦ 𝐶 ) ) = ( 𝑀 Σg ∅ )
16 1 gsum0 ⊢ ( 𝑀 Σg ∅ ) = 𝑍
17 15 16 eqtri ⊢ ( 𝑀 Σg ( 𝑦 ∈ ∅ ↦ 𝐶 ) ) = 𝑍
18 mpteq1 ⊢ ( 𝐵 = ∅ → ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑦 ∈ ∅ ↦ 𝐶 ) )
19 18 oveq2d ⊢ ( 𝐵 = ∅ → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) = ( 𝑀 Σg ( 𝑦 ∈ ∅ ↦ 𝐶 ) ) )
20 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 = ∅ ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) = ( 𝑀 Σg ( 𝑦 ∈ ∅ ↦ 𝐶 ) ) )
21 1 gsumz ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐵 ∈ 𝑊 ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) = 𝑍 )
22 2 3 21 syl2anc ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) = 𝑍 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) = 𝑍 )
24 23 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 = ∅ ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) = 𝑍 )
25 17 20 24 3eqtr4a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 = ∅ ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) = ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) )
26 nfv ⊢ Ⅎ 𝑦 𝜑
27 nfcv ⊢ Ⅎ 𝑦 𝐴
28 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 )
29 27 28 nfdif ⊢ Ⅎ 𝑦 ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) )
30 29 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) )
31 26 30 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
32 nfv ⊢ Ⅎ 𝑦 𝐵 ≠ ∅
33 31 32 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ )
34 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
35 iindif2 ⊢ ( 𝐵 ≠ ∅ → ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) = ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
36 35 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) = ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
37 34 36 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
38 eliin ⊢ ( 𝑥 ∈ ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) → ( 𝑥 ∈ ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ↔ ∀ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) )
39 38 ibi ⊢ ( 𝑥 ∈ ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) → ∀ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
40 39 r19.21bi ⊢ ( ( 𝑥 ∈ ∩ 𝑦 ∈ 𝐵 ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
41 37 40 sylancom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐴 ∖ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
42 41 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ¬ 𝑥 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) )
43 34 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
44 nfv ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 )
45 5 an32s ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
46 45 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑋 )
47 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
48 44 46 47 fnmptd ⊢ ( ( ( 𝜑 ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
49 48 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
50 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝐴 ∈ 𝑉 )
51 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
52 51 1 mndidcl ⊢ ( 𝑀 ∈ Mnd → 𝑍 ∈ ( Base ‘ 𝑀 ) )
53 2 52 syl ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑀 ) )
54 53 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝑍 ∈ ( Base ‘ 𝑀 ) )
55 elsuppfn ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 𝑍 ) ) )
56 49 50 54 55 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 𝑍 ) ) )
57 43 56 mpbirand ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 𝑍 ) )
58 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ⊆ 𝐴 )
59 58 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) → 𝑥 ∈ 𝐴 )
60 59 5 syldanl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑋 )
61 60 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝑋 )
62 47 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
63 43 61 62 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) = 𝐶 )
64 63 neeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑥 ) ≠ 𝑍 ↔ 𝐶 ≠ 𝑍 ) )
65 57 64 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ↔ 𝐶 ≠ 𝑍 ) )
66 65 necon2bbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐶 = 𝑍 ↔ ¬ 𝑥 ∈ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) )
67 42 66 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 = 𝑍 )
68 33 67 mpteq2da ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) → ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) )
69 68 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) ∧ 𝐵 ≠ ∅ ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) = ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) )
70 25 69 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) = ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝑍 ) ) )
71 70 23 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) ) ) → ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) = 𝑍 )
72 6 7 13 71 4 suppss2f ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑀 Σg ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ) ) supp 𝑍 ) ⊆ ∪ 𝑦 ∈ 𝐵 ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) supp 𝑍 ) )