Metamath Proof Explorer

Theorem sge0iunmptlemfi

Description: Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iunmptlemfi.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
sge0iunmptlemfi.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
sge0iunmptlemfi.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
sge0iunmptlemfi.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
sge0iunmptlemfi.re ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
Assertion sge0iunmptlemfi ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0iunmptlemfi.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 sge0iunmptlemfi.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 sge0iunmptlemfi.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
4 sge0iunmptlemfi.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
5 sge0iunmptlemfi.re ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
6 iuneq1 ⊢ ( 𝑦 = ∅ → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 )
7 6 mpteq1d ⊢ ( 𝑦 = ∅ → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) )
8 7 fveq2d ⊢ ( 𝑦 = ∅ → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) ) )
9 mpteq1 ⊢ ( 𝑦 = ∅ → ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
10 9 fveq2d ⊢ ( 𝑦 = ∅ → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
11 8 10 eqeq12d ⊢ ( 𝑦 = ∅ → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
12 iuneq1 ⊢ ( 𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ 𝑧 𝐵 )
13 12 mpteq1d ⊢ ( 𝑦 = 𝑧 → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) )
14 13 fveq2d ⊢ ( 𝑦 = 𝑧 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) )
15 mpteq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
16 15 fveq2d ⊢ ( 𝑦 = 𝑧 → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
17 14 16 eqeq12d ⊢ ( 𝑦 = 𝑧 → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
18 iuneq1 ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 )
19 18 mpteq1d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) )
20 19 fveq2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) )
21 mpteq1 ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
22 21 fveq2d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
23 20 22 eqeq12d ⊢ ( 𝑦 = ( 𝑧 ∪ { 𝑤 } ) → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
24 iuneq1 ⊢ ( 𝑦 = 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )
25 24 mpteq1d ⊢ ( 𝑦 = 𝐴 → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) )
26 25 fveq2d ⊢ ( 𝑦 = 𝐴 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) )
27 mpteq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
28 27 fveq2d ⊢ ( 𝑦 = 𝐴 → ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
29 26 28 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑦 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ↔ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
30 0iun ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
31 mpteq1 ⊢ ( ∪ 𝑥 ∈ ∅ 𝐵 = ∅ → ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∅ ↦ 𝐶 ) )
32 30 31 ax-mp ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∅ ↦ 𝐶 )
33 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ 𝐶 ) = ∅
34 32 33 eqtri ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) = ∅
35 34 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ∅ )
36 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ∅
37 36 fveq2i ⊢ ( Σ^ ‘ ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ∅ )
38 35 37 eqtr4i ⊢ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
39 38 a1i ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ∅ ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
40 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) )
41 nfcv ⊢ Ⅎ 𝑥 Σ^
42 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ { 𝑤 } 𝐵
43 nfcv ⊢ Ⅎ 𝑥 𝐶
44 42 43 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 )
45 41 44 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) )
46 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → 𝑧 ⊆ 𝐴 )
47 1 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → 𝐴 ∈ Fin )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → 𝑧 ⊆ 𝐴 )
49 ssfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑧 ⊆ 𝐴 ) → 𝑧 ∈ Fin )
50 47 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → 𝑧 ∈ Fin )
51 46 50 syldan ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → 𝑧 ∈ Fin )
52 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) )
53 eldifn ⊢ ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) → ¬ 𝑤 ∈ 𝑧 )
54 disjsn ⊢ ( ( 𝑧 ∩ { 𝑤 } ) = ∅ ↔ ¬ 𝑤 ∈ 𝑧 )
55 53 54 sylibr ⊢ ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) → ( 𝑧 ∩ { 𝑤 } ) = ∅ )
56 55 adantl ⊢ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( 𝑧 ∩ { 𝑤 } ) = ∅ )
57 56 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( 𝑧 ∩ { 𝑤 } ) = ∅ )
58 57 54 sylib ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ¬ 𝑤 ∈ 𝑧 )
59 simpll ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → 𝜑 )
60 ssel2 ⊢ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
61 60 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
62 59 61 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
63 62 recnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℂ )
64 63 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℂ )
65 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
66 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
67 vex ⊢ 𝑤 ∈ V
68 66 67 65 iunxsnf ⊢ ∪ 𝑥 ∈ { 𝑤 } 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵
69 65 68 eqtr4di ⊢ ( 𝑥 = 𝑤 → 𝐵 = ∪ 𝑥 ∈ { 𝑤 } 𝐵 )
70 69 mpteq1d ⊢ ( 𝑥 = 𝑤 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) )
71 70 fveq2d ⊢ ( 𝑥 = 𝑤 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) )
72 68 mpteq1i ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 )
73 72 a1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) )
74 73 fveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) )
75 eldifi ⊢ ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) → 𝑤 ∈ 𝐴 )
76 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ 𝐴 )
77 66 43 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 )
78 41 77 nffv ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) )
79 nfcv ⊢ Ⅎ 𝑥 ℝ
80 78 79 nfel ⊢ Ⅎ 𝑥 ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ℝ
81 76 80 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
82 eleq1w ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
83 82 anbi2d ⊢ ( 𝑥 = 𝑤 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) ) )
84 70 72 eqtrdi ⊢ ( 𝑥 = 𝑤 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) )
85 84 fveq2d ⊢ ( 𝑥 = 𝑤 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) )
86 85 eleq1d ⊢ ( 𝑥 = 𝑤 → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ↔ ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ) )
87 83 86 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ) ) )
88 81 87 5 chvarfv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
89 75 88 sylan2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( Σ^ ‘ ( 𝑘 ∈ ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
90 74 89 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
91 90 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
92 91 recnd ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ∈ ℂ )
93 40 45 51 52 58 64 71 92 fsumsplitsn ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
94 93 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
95 94 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
96 iunxun ⊢ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 )
97 96 mpteq1i ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) ↦ 𝐶 )
98 97 fveq2i ⊢ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) ↦ 𝐶 ) )
99 98 a1i ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑘 ∈ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) ↦ 𝐶 ) ) )
100 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) )
101 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
102 iunexg ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
103 1 101 102 syl2anc ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
105 iunss1 ⊢ ( 𝑧 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑧 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
106 105 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ∪ 𝑥 ∈ 𝑧 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
107 104 106 ssexd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ∪ 𝑥 ∈ 𝑧 𝐵 ∈ V )
108 107 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ∪ 𝑥 ∈ 𝑧 𝐵 ∈ V )
109 103 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
110 snssi ⊢ ( 𝑤 ∈ 𝐴 → { 𝑤 } ⊆ 𝐴 )
111 75 110 syl ⊢ ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) → { 𝑤 } ⊆ 𝐴 )
112 iunss1 ⊢ ( { 𝑤 } ⊆ 𝐴 → ∪ 𝑥 ∈ { 𝑤 } 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
113 111 112 syl ⊢ ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) → ∪ 𝑥 ∈ { 𝑤 } 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
114 113 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ∪ 𝑥 ∈ { 𝑤 } 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
115 109 114 ssexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ∪ 𝑥 ∈ { 𝑤 } 𝐵 ∈ V )
116 115 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ∪ 𝑥 ∈ { 𝑤 } 𝐵 ∈ V )
117 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → Disj 𝑥 ∈ 𝐴 𝐵 )
118 111 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → { 𝑤 } ⊆ 𝐴 )
119 disjiun ⊢ ( ( Disj 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑧 ⊆ 𝐴 ∧ { 𝑤 } ⊆ 𝐴 ∧ ( 𝑧 ∩ { 𝑤 } ) = ∅ ) ) → ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) = ∅ )
120 117 46 118 57 119 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( ∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) = ∅ )
121 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↔ ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 )
122 121 bilani ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 )
123 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝜑 )
124 61 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
125 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
126 123 124 125 4 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
127 126 3exp ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
128 127 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → ( ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
130 122 129 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
131 130 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
132 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↔ ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 )
133 132 bilani ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 )
134 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝜑 )
135 111 sselda ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ { 𝑤 } ) → 𝑥 ∈ 𝐴 )
136 135 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ) → 𝑥 ∈ 𝐴 )
137 136 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
138 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
139 134 137 138 4 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
140 139 3exp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( 𝑥 ∈ { 𝑤 } → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
141 140 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
142 141 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → ( ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
143 133 142 mpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
144 143 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
145 100 108 116 120 131 144 sge0splitmpt ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
146 99 145 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
147 146 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
148 id ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
149 148 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
150 4 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
151 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
152 150 151 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
153 2 152 sge0ge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
154 5 153 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
155 elrege0 ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
156 154 155 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
157 59 61 156 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
158 eqid ⊢ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
159 157 158 fmptd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) : 𝑧 ⟶ ( 0 [,) +∞ ) )
160 50 159 sge0fsum ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) )
161 160 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) )
162 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) )
163 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
164 nfcv ⊢ Ⅎ 𝑥 𝑦
165 163 164 nffv ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 )
166 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 )
167 162 165 166 cbvsum ⊢ Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 )
168 167 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) )
169 id ⊢ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑧 )
170 fvexd ⊢ ( 𝑥 ∈ 𝑧 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ V )
171 158 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑧 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ V ) → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
172 169 170 171 syl2anc ⊢ ( 𝑥 ∈ 𝑧 → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
173 172 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
174 173 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
175 174 sumeq2d ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
176 168 175 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
177 176 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
178 149 161 177 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
179 178 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
180 179 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
181 50 62 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
182 181 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
183 rexadd ⊢ ( ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ∈ ℝ ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
184 182 91 183 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
185 184 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
186 147 180 185 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
187 snfi ⊢ { 𝑤 } ∈ Fin
188 187 a1i ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → { 𝑤 } ∈ Fin )
189 unfi ⊢ ( ( 𝑧 ∈ Fin ∧ { 𝑤 } ∈ Fin ) → ( 𝑧 ∪ { 𝑤 } ) ∈ Fin )
190 51 188 189 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( 𝑧 ∪ { 𝑤 } ) ∈ Fin )
191 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝜑 )
192 60 ad4ant14 ⊢ ( ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
193 simpll ⊢ ( ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) )
194 elunnel1 ⊢ ( ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ { 𝑤 } )
195 elsni ⊢ ( 𝑥 ∈ { 𝑤 } → 𝑥 = 𝑤 )
196 194 195 syl ⊢ ( ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 = 𝑤 )
197 196 adantll ⊢ ( ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 = 𝑤 )
198 simpr ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 = 𝑤 ) → 𝑥 = 𝑤 )
199 75 adantr ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 = 𝑤 ) → 𝑤 ∈ 𝐴 )
200 198 199 eqeltrd ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 = 𝑤 ) → 𝑥 ∈ 𝐴 )
201 193 197 200 syl2anc ⊢ ( ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
202 201 adantlll ⊢ ( ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
203 192 202 pm2.61dan ⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝑥 ∈ 𝐴 )
204 203 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝑥 ∈ 𝐴 )
205 191 204 156 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
206 190 205 sge0fsummpt ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
207 206 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
208 95 186 207 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
209 208 ex ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
210 11 17 23 29 39 209 1 findcard2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )