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 biimpi ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 → ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 )
123 122 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 )
124 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝜑 )
125 61 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
126 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
127 124 125 126 4 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
128 127 3exp ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝑧 → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
129 128 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
130 129 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → ( ∃ 𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
131 123 130 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
132 131 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
133 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↔ ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 )
134 133 biimpi ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 → ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 )
135 134 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 )
136 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝜑 )
137 111 sselda ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ { 𝑤 } ) → 𝑥 ∈ 𝐴 )
138 137 adantll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ) → 𝑥 ∈ 𝐴 )
139 138 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
140 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
141 136 139 140 4 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ { 𝑤 } ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
142 141 3exp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( 𝑥 ∈ { 𝑤 } → ( 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) ) )
143 142 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) → ( ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
144 143 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → ( ∃ 𝑥 ∈ { 𝑤 } 𝑘 ∈ 𝐵 → 𝐶 ∈ ( 0 [,] +∞ ) ) )
145 135 144 mpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
146 145 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
147 100 108 116 120 132 146 sge0splitmpt ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ( ∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ) ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
148 99 147 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
149 148 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
150 id ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
151 150 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
152 4 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
153 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
154 152 153 fmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
155 2 154 sge0ge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
156 5 155 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
157 elrege0 ⊢ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ∧ 0 ≤ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) )
158 156 157 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
159 59 61 158 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
160 eqid ⊢ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
161 159 160 fmptd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) : 𝑧 ⟶ ( 0 [,) +∞ ) )
162 50 161 sge0fsum ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) )
163 162 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) )
164 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) )
165 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
166 nfcv ⊢ Ⅎ 𝑥 𝑦
167 165 166 nffv ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 )
168 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 )
169 164 167 168 cbvsum ⊢ Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 )
170 169 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) )
171 id ⊢ ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑧 )
172 fvexd ⊢ ( 𝑥 ∈ 𝑧 → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ V )
173 160 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑧 ∧ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ V ) → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
174 171 172 173 syl2anc ⊢ ( 𝑥 ∈ 𝑧 → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
175 174 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
176 175 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
177 176 sumeq2d ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑥 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑥 ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
178 170 177 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
179 178 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → Σ 𝑦 ∈ 𝑧 ( ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ‘ 𝑦 ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
180 151 163 179 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
181 180 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
182 181 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
183 50 62 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐴 ) → Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
184 183 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ )
185 rexadd ⊢ ( ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ℝ ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ∈ ℝ ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
186 184 91 185 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
187 186 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) +𝑒 ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
188 149 182 187 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ 𝑥 ∈ 𝑧 ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) + ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ { 𝑤 } 𝐵 ↦ 𝐶 ) ) ) )
189 snfi ⊢ { 𝑤 } ∈ Fin
190 189 a1i ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → { 𝑤 } ∈ Fin )
191 unfi ⊢ ( ( 𝑧 ∈ Fin ∧ { 𝑤 } ∈ Fin ) → ( 𝑧 ∪ { 𝑤 } ) ∈ Fin )
192 51 190 191 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( 𝑧 ∪ { 𝑤 } ) ∈ Fin )
193 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝜑 )
194 60 ad4ant14 ⊢ ( ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
195 simpll ⊢ ( ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) )
196 elunnel1 ⊢ ( ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ { 𝑤 } )
197 elsni ⊢ ( 𝑥 ∈ { 𝑤 } → 𝑥 = 𝑤 )
198 196 197 syl ⊢ ( ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 = 𝑤 )
199 198 adantll ⊢ ( ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 = 𝑤 )
200 simpr ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 = 𝑤 ) → 𝑥 = 𝑤 )
201 75 adantr ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 = 𝑤 ) → 𝑤 ∈ 𝐴 )
202 200 201 eqeltrd ⊢ ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 = 𝑤 ) → 𝑥 ∈ 𝐴 )
203 195 199 202 syl2anc ⊢ ( ( ( 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
204 203 adantlll ⊢ ( ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) ∧ ¬ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐴 )
205 194 204 pm2.61dan ⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝑥 ∈ 𝐴 )
206 205 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → 𝑥 ∈ 𝐴 )
207 193 206 158 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ∈ ( 0 [,) +∞ ) )
208 192 207 sge0fsummpt ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
209 208 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = Σ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) )
210 95 188 209 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) ∧ ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )
211 210 ex ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ ( 𝐴 ∖ 𝑧 ) ) ) → ( ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑧 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ ( 𝑧 ∪ { 𝑤 } ) ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) ) )
212 11 17 23 29 39 211 1 findcard2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) )