sge0iunmptlemfi - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sge0iunmptlemfi		Structured version Visualization version GIF version

Theorem sge0iunmptlemfi 46865

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.)

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

**Assertion**
Ref	Expression
sge0iunmptlemfi	⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Distinct variable groups: 𝐴,𝑘,𝑥 𝐵,𝑘 𝑥,𝐶 𝜑,𝑘,𝑥 Allowed substitution hints: 𝐵(𝑥) 𝐶(𝑘) 𝑉(𝑥,𝑘)

Proof of Theorem sge0iunmptlemfi Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iuneq1 4951	. . . . 5 ⊢ (𝑦 = ∅ → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵)
2	1	mpteq1d 5176	. . . 4 ⊢ (𝑦 = ∅ → (𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶))
3	2	fveq2d 6840	. . 3 ⊢ (𝑦 = ∅ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶)))
4		mpteq1 5175	. . . 4 ⊢ (𝑦 = ∅ → (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
5	4	fveq2d 6840	. . 3 ⊢ (𝑦 = ∅ → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
6	3, 5	eqeq12d 2753	. 2 ⊢ (𝑦 = ∅ → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
7		iuneq1 4951	. . . . 5 ⊢ (𝑦 = 𝑧 → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ 𝑧 𝐵)
8	7	mpteq1d 5176	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶))
9	8	fveq2d 6840	. . 3 ⊢ (𝑦 = 𝑧 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)))
10		mpteq1 5175	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
11	10	fveq2d 6840	. . 3 ⊢ (𝑦 = 𝑧 → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
12	9, 11	eqeq12d 2753	. 2 ⊢ (𝑦 = 𝑧 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
13		iuneq1 4951	. . . . 5 ⊢ (𝑦 = (𝑧 ∪ {𝑤}) → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵)
14	13	mpteq1d 5176	. . . 4 ⊢ (𝑦 = (𝑧 ∪ {𝑤}) → (𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶))
15	14	fveq2d 6840	. . 3 ⊢ (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)))
16		mpteq1 5175	. . . 4 ⊢ (𝑦 = (𝑧 ∪ {𝑤}) → (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
17	16	fveq2d 6840	. . 3 ⊢ (𝑦 = (𝑧 ∪ {𝑤}) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
18	15, 17	eqeq12d 2753	. 2 ⊢ (𝑦 = (𝑧 ∪ {𝑤}) → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
19		iuneq1 4951	. . . . 5 ⊢ (𝑦 = 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵)
20	19	mpteq1d 5176	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))
21	20	fveq2d 6840	. . 3 ⊢ (𝑦 = 𝐴 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
22		mpteq1 5175	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
23	22	fveq2d 6840	. . 3 ⊢ (𝑦 = 𝐴 → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
24	21, 23	eqeq12d 2753	. 2 ⊢ (𝑦 = 𝐴 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
25		0iun 5006	. . . . . . 7 ⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅
26		mpteq1 5175	. . . . . . 7 ⊢ (∪ 𝑥 ∈ ∅ 𝐵 = ∅ → (𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶) = (𝑘 ∈ ∅ ↦ 𝐶))
27	25, 26	ax-mp 5	. . . . . 6 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶) = (𝑘 ∈ ∅ ↦ 𝐶)
28		mpt0 6636	. . . . . 6 ⊢ (𝑘 ∈ ∅ ↦ 𝐶) = ∅
29	27, 28	eqtri 2760	. . . . 5 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶) = ∅
30	29	fveq2i 6839	. . . 4 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶)) = (Σ^{^}‘∅)
31		mpt0 6636	. . . . 5 ⊢ (𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = ∅
32	31	fveq2i 6839	. . . 4 ⊢ (Σ^{^}‘(𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘∅)
33	30, 32	eqtr4i 2763	. . 3 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
34	33	a1i 11	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ ∅ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ ∅ ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
35		nfv 1916	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)))
36		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥Σ^{^}
37		nfiu1 4970	. . . . . . . . 9 ⊢ Ⅎ𝑥∪ 𝑥 ∈ {𝑤}𝐵
38		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑥𝐶
39	37, 38	nfmpt 5184	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)
40	36, 39	nffv 6846	. . . . . . 7 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))
41		simprl 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → 𝑧 ⊆ 𝐴)
42		sge0iunmptlemfi.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ Fin)
43	42	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → 𝐴 ∈ Fin)
44		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → 𝑧 ⊆ 𝐴)
45		ssfi 9102	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin ∧ 𝑧 ⊆ 𝐴) → 𝑧 ∈ Fin)
46	43, 44, 45	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → 𝑧 ∈ Fin)
47	41, 46	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → 𝑧 ∈ Fin)
48		simprr 773	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → 𝑤 ∈ (𝐴 ∖ 𝑧))
49		eldifn 4073	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (𝐴 ∖ 𝑧) → ¬ 𝑤 ∈ 𝑧)
50		disjsn 4656	. . . . . . . . . . 11 ⊢ ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤 ∈ 𝑧)
51	49, 50	sylibr 234	. . . . . . . . . 10 ⊢ (𝑤 ∈ (𝐴 ∖ 𝑧) → (𝑧 ∩ {𝑤}) = ∅)
52	51	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (𝑧 ∩ {𝑤}) = ∅)
53	52	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (𝑧 ∩ {𝑤}) = ∅)
54	53, 50	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → ¬ 𝑤 ∈ 𝑧)
55		simpll 767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧) → 𝜑)
56		ssel2 3917	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴)
57	56	adantll 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴)
58		sge0iunmptlemfi.re	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
59	55, 57, 58	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
60	59	recnd 11168	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℂ)
61	60	adantlrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ 𝑥 ∈ 𝑧) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℂ)
62		csbeq1a 3852	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
63		nfcsb1v 3862	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
64		vex 3434	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
65	63, 64, 62	iunxsnf 45519	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ {𝑤}𝐵 = ⦋𝑤 / 𝑥⦌𝐵
66	62, 65	eqtr4di 2790	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → 𝐵 = ∪ 𝑥 ∈ {𝑤}𝐵)
67	66	mpteq1d 5176	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))
68	67	fveq2d 6840	. . . . . . 7 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)))
69	65	mpteq1i 5177	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)
70	69	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶))
71	70	fveq2d 6840	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)))
72		eldifi 4072	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (𝐴 ∖ 𝑧) → 𝑤 ∈ 𝐴)
73		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴)
74	63, 38	nfmpt 5184	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)
75	36, 74	nffv 6846	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶))
76		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥ℝ
77	75, 76	nfel 2914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ ℝ
78	73, 77	nfim 1898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ ℝ)
79		eleq1w 2820	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
80	79	anbi2d 631	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴)))
81	67, 69	eqtrdi 2788	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶))
82	81	fveq2d 6840	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)))
83	82	eleq1d 2822	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑤 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ ↔ (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ ℝ))
84	80, 83	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ ℝ)))
85	78, 84, 58	chvarfv 2248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ ℝ)
86	72, 85	sylan2 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (Σ^{^}‘(𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ ℝ)
87	71, 86	eqeltrd 2837	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)) ∈ ℝ)
88	87	adantrl 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)) ∈ ℝ)
89	88	recnd 11168	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)) ∈ ℂ)
90	35, 40, 47, 48, 54, 61, 68, 89	fsumsplitsn 15701	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
91	90	eqcomd 2743	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
92	91	adantr 480	. . . 4 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
93		iunxun 5037	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = (∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ {𝑤}𝐵)
94	93	mpteq1i 5177	. . . . . . . . 9 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶) = (𝑘 ∈ (∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)
95	94	fveq2i 6839	. . . . . . . 8 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶))
96	95	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)))
97		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑘(𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)))
98		sge0iunmptlemfi.b	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)
99	98	ralrimiva 3130	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉)
100		iunexg 7911	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
101	42, 99, 100	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
102	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
103		iunss1 4949	. . . . . . . . . . 11 ⊢ (𝑧 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑧 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
104	103	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → ∪ 𝑥 ∈ 𝑧 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
105	102, 104	ssexd 5262	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → ∪ 𝑥 ∈ 𝑧 𝐵 ∈ V)
106	105	adantrr 718	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → ∪ 𝑥 ∈ 𝑧 𝐵 ∈ V)
107	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
108		snssi 4752	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ 𝐴 → {𝑤} ⊆ 𝐴)
109	72, 108	syl 17	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ (𝐴 ∖ 𝑧) → {𝑤} ⊆ 𝐴)
110		iunss1 4949	. . . . . . . . . . . 12 ⊢ ({𝑤} ⊆ 𝐴 → ∪ 𝑥 ∈ {𝑤}𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
111	109, 110	syl 17	. . . . . . . . . . 11 ⊢ (𝑤 ∈ (𝐴 ∖ 𝑧) → ∪ 𝑥 ∈ {𝑤}𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
112	111	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → ∪ 𝑥 ∈ {𝑤}𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
113	107, 112	ssexd 5262	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → ∪ 𝑥 ∈ {𝑤}𝐵 ∈ V)
114	113	adantrl 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → ∪ 𝑥 ∈ {𝑤}𝐵 ∈ V)
115		sge0iunmptlemfi.dj	. . . . . . . . . 10 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
116	115	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → Disj 𝑥 ∈ 𝐴 𝐵)
117	109	ad2antll 730	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → {𝑤} ⊆ 𝐴)
118		disjiun 5074	. . . . . . . . 9 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑧 ⊆ 𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → (∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ {𝑤}𝐵) = ∅)
119	116, 41, 117, 53, 118	syl13anc 1375	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪ 𝑥 ∈ {𝑤}𝐵) = ∅)
120		eliun 4938	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↔ ∃𝑥 ∈ 𝑧 𝑘 ∈ 𝐵)
121	120	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 → ∃𝑥 ∈ 𝑧 𝑘 ∈ 𝐵)
122	121	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵) → ∃𝑥 ∈ 𝑧 𝑘 ∈ 𝐵)
123		simp1l 1199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵) → 𝜑)
124	57	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵) → 𝑥 ∈ 𝐴)
125		simp3 1139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
126		sge0iunmptlemfi.c	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
127	123, 124, 125, 126	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
128	127	3exp 1120	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → (𝑥 ∈ 𝑧 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
129	128	rexlimdv 3137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → (∃𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
130	129	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵) → (∃𝑥 ∈ 𝑧 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
131	122, 130	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
132	131	adantlrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵) → 𝐶 ∈ (0[,]+∞))
133		eliun 4938	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↔ ∃𝑥 ∈ {𝑤}𝑘 ∈ 𝐵)
134	133	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 → ∃𝑥 ∈ {𝑤}𝑘 ∈ 𝐵)
135	134	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵) → ∃𝑥 ∈ {𝑤}𝑘 ∈ 𝐵)
136		simp1l 1199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘 ∈ 𝐵) → 𝜑)
137	109	sselda 3922	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 ∈ {𝑤}) → 𝑥 ∈ 𝐴)
138	137	adantll 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ {𝑤}) → 𝑥 ∈ 𝐴)
139	138	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘 ∈ 𝐵) → 𝑥 ∈ 𝐴)
140		simp3 1139	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
141	136, 139, 140, 126	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ {𝑤} ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
142	141	3exp 1120	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (𝑥 ∈ {𝑤} → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
143	142	rexlimdv 3137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) → (∃𝑥 ∈ {𝑤}𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
144	143	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵) → (∃𝑥 ∈ {𝑤}𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
145	135, 144	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
146	145	adantlrl 721	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ 𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵) → 𝐶 ∈ (0[,]+∞))
147	97, 106, 114, 119, 132, 146	sge0splitmpt 46863	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ^{^}‘(𝑘 ∈ (∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪ 𝑥 ∈ {𝑤}𝐵) ↦ 𝐶)) = ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
148	96, 147	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
149	148	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
150		id 22	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
151	150	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
152	126	3expa 1119	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
153		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
154	152, 153	fmptd 7062	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
155	98, 154	sge0ge0 46836	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
156	58, 155	jca 511	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
157		elrege0 13402	. . . . . . . . . . . . 13 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞) ↔ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ ∧ 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
158	156, 157	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
159	55, 57, 158	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
160		eqid 2737	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
161	159, 160	fmptd 7062	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → (𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝑧⟶(0[,)+∞))
162	46, 161	sge0fsum 46839	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑦 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦))
163	162	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑦 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦))
164		fveq2 6836	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦) = ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥))
165		nfmpt1 5185	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
166		nfcv 2899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑦
167	165, 166	nffv 6846	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦)
168		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥)
169	164, 167, 168	cbvsum 15652	. . . . . . . . . . 11 ⊢ Σ𝑦 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦) = Σ𝑥 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥)
170	169	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → Σ𝑦 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦) = Σ𝑥 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥))
171		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑧)
172		fvexd 6851	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝑧 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V)
173	160	fvmpt2 6955	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑧 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) → ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥) = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
174	171, 172, 173	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑧 → ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥) = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
175	174	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥) = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
176	175	ralrimiva 3130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → ∀𝑥 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥) = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
177	176	sumeq2d 15658	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → Σ𝑥 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑥) = Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
178	170, 177	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → Σ𝑦 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦) = Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
179	178	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → Σ𝑦 ∈ 𝑧 ((𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))‘𝑦) = Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
180	151, 163, 179	3eqtrd 2776	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ⊆ 𝐴) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
181	180	adantlrr 722	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
182	181	oveq1d 7377	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))) = (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
183	46, 59	fsumrecl 15691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐴) → Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
184	183	adantrr 718	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
185		rexadd 13179	. . . . . . 7 ⊢ ((Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶)) ∈ ℝ) → (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))) = (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
186	184, 88, 185	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))) = (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
187	186	adantr 480	. . . . 5 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) +_𝑒 (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))) = (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
188	149, 182, 187	3eqtrd 2776	. . . 4 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = (Σ𝑥 ∈ 𝑧 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) + (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ {𝑤}𝐵 ↦ 𝐶))))
189		snfi 8985	. . . . . . . 8 ⊢ {𝑤} ∈ Fin
190	189	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → {𝑤} ∈ Fin)
191		unfi 9100	. . . . . . 7 ⊢ ((𝑧 ∈ Fin ∧ {𝑤} ∈ Fin) → (𝑧 ∪ {𝑤}) ∈ Fin)
192	47, 190, 191	syl2anc 585	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (𝑧 ∪ {𝑤}) ∈ Fin)
193		simpll 767	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝜑)
194	56	ad4ant14 753	. . . . . . . . 9 ⊢ ((((𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴)
195		simpll 767	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥 ∈ 𝑧) → 𝑤 ∈ (𝐴 ∖ 𝑧))
196		elunnel1 4095	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥 ∈ 𝑧) → 𝑥 ∈ {𝑤})
197		elsni 4585	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑤} → 𝑥 = 𝑤)
198	196, 197	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑧 ∪ {𝑤}) ∧ ¬ 𝑥 ∈ 𝑧) → 𝑥 = 𝑤)
199	198	adantll 715	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥 ∈ 𝑧) → 𝑥 = 𝑤)
200		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
201	72	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 = 𝑤) → 𝑤 ∈ 𝐴)
202	200, 201	eqeltrd 2837	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 = 𝑤) → 𝑥 ∈ 𝐴)
203	195, 199, 202	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝑤 ∈ (𝐴 ∖ 𝑧) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴)
204	203	adantlll 719	. . . . . . . . 9 ⊢ ((((𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) ∧ ¬ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐴)
205	194, 204	pm2.61dan 813	. . . . . . . 8 ⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧)) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥 ∈ 𝐴)
206	205	adantll 715	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥 ∈ 𝐴)
207	193, 206, 158	syl2anc 585	. . . . . 6 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
208	192, 207	sge0fsummpt 46842	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → (Σ^{^}‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
209	208	adantr 480	. . . 4 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ (𝑧 ∪ {𝑤})(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
210	92, 188, 209	3eqtr4d 2782	. . 3 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
211	210	ex 412	. 2 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐴 ∧ 𝑤 ∈ (𝐴 ∖ 𝑧))) → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑧 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑧 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ (𝑧 ∪ {𝑤}) ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
212	6, 12, 18, 24, 34, 211, 42	findcard2d 9096	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ⦋csb 3838 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 {csn 4568 ∪ ciun 4934 Disj wdisj 5053 class class class wbr 5086 ↦ cmpt 5167 ‘cfv 6494 (class class class)co 7362 Fincfn 8888 ℂcc 11031 ℝcr 11032 0cc0 11033 + caddc 11036 +∞cpnf 11171 ≤ cle 11175 +_𝑒 cxad 13056 [,)cico 13295 [,]cicc 13296 Σcsu 15643 Σ^{^}csumge0 46814

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-inf2 9557 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-se 5580 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-isom 6503 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-er 8638 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-sup 9350 df-oi 9420 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-xadd 13059 df-ico 13299 df-icc 13300 df-fz 13457 df-fzo 13604 df-seq 13959 df-exp 14019 df-hash 14288 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-clim 15445 df-sum 15644 df-sumge0 46815

This theorem is referenced by: sge0iunmptlemre 46867

W3C validator