sge0iunmpt - Mathbox for Glauco Siliprandi

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

Theorem sge0iunmpt 47428

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
sge0iunmpt.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sge0iunmpt.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
sge0iunmpt.dj	⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
sge0iunmpt.c	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))

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

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

Proof of Theorem sge0iunmpt Dummy variables 𝑗 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1946	. . . 4 ⊢ Ⅎ𝑥𝜑
2		nfcv 2922	. . . . . 6 ⊢ Ⅎ𝑥Σ^{^}
3		nfiu1 4985	. . . . . . 7 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
5	3, 4	nfmpt 5202	. . . . . 6 ⊢ Ⅎ𝑥(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
6	2, 5	nffv 6895	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))
7		nfmpt1 5203	. . . . . 6 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
8	2, 7	nffv 6895	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
9	6, 8	nfeq 2935	. . . 4 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
10		sge0iunmpt.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
11		sge0iunmpt.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
12	11	ralrimiva 3154	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
13		iunexg 7975	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
14	10, 12, 13	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
15		eliun 4954	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
16	15	bilani 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
17		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑘
18	17, 3	nfel 2936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
19	1, 18	nfan 1931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
20	4	nfel1 2938	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,]+∞)
21		sge0iunmpt.c	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
22	21	3exp 1137	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
23	22	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
24	19, 20, 23	rexlimd 3269	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
25	16, 24	mpd 16	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
26		eqid 2760	. . . . . . . . . 10 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
27	25, 26	fmptd 7114	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
28	14, 27	sge0xrcl 47395	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
29	28	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
30		id 23	. . . . . . . . . . 11 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
31	30	eqcomd 2766	. . . . . . . . . 10 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
32	31	adantl 487	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
33	32	3adant1 1148	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
34	14	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
35	25	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
36		ssiun2 5005	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
37	36	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	34, 35, 37	sge0lessmpt 47409	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
39	38	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
40	33, 39	eqbrtrd 5126	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
41	29, 40	xrgepnfd 46343	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞)
42	10	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉)
43		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴)
44		nfcsb1v 3870	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
45		nfcsb1v 3870	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊
46	44, 45	nfel 2936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊
47	43, 46	nfim 1928	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
48		eleq1w 2843	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
49	48	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴)))
50		csbeq1a 3860	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
51		csbeq1a 3860	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝑊 = ⦋𝑦 / 𝑥⦌𝑊)
52	50, 51	eleq12d 2854	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊))
53	49, 52	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)))
54	47, 53, 11	chvarfv 2276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
55	54	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
56	44, 4	nfmpt 5202	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)
57		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(0[,]+∞)
58	56, 44, 57	nff 6705	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)
59	43, 58	nfim 1928	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
60	50	mpteq1d 5194	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
61	60, 50	feq12d 6697	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)))
62	49, 61	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))))
63	22	imp31 423	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
64		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
65	63, 64	fmptd 7114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
66	59, 62, 65	chvarfv 2276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
67	66	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
68	55, 67	sge0cl 47391	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
69		nfcv 2922	. . . . . . . . . 10 ⊢ Ⅎ𝑦(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))
70	2, 56	nffv 6895	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
71	60	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
72	69, 70, 71	cbvmpt 5206	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
73	68, 72	fmptd 7114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
74	73	3adant3 1150	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
75		id 23	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
76		fvexd 6900	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V)
77		eqid 2760	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
78	77	elrnmpt1 5941	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
79	75, 76, 78	syl2anc 596	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
80	79	adantr 486	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
81	32, 80	eqeltrd 2860	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
82	81	3adant1 1148	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
83	42, 74, 82	sge0pnfval 47383	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞)
84	41, 83	eqtr4d 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
85	84	3exp 1137	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))))
86	1, 9, 85	rexlimd 3269	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
87	86	imp 412	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
88		simpl 488	. . 3 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝜑)
89		ralnex 3088	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
90		df-ne 2956	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
91	90	bicomi 227	. . . . . 6 ⊢ (¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
92	91	ralbii 3108	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
93	89, 92	sylbb1 240	. . . 4 ⊢ (¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
94	93	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
95	10	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝐴 ∈ 𝑉)
96		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑊
97	44, 96	nfel 2936	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊
98	43, 97	nfim 1928	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
99	50	eleq1d 2845	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊))
100	49, 99	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)))
101	98, 100, 11	chvarfv 2276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
102	101	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
103		sge0iunmpt.dj	. . . . . . 7 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
104		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
105	104, 44, 50	cbvdisj 5079	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
106	103, 105	sylib 221	. . . . . 6 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
107	106	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
108		nfv 1946	. . . . . . . 8 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
109		nfcsb1v 3870	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶
110	109	nfel1 2938	. . . . . . . 8 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)
111	108, 110	nfim 1928	. . . . . . 7 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
112		eleq1w 2843	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵))
113	112	3anbi3d 1470	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)))
114		csbeq1a 3860	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑘⦌𝐶)
115	114	eleq1d 2845	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔ ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
116	113, 115	imbi12d 347	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
117		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
118	17, 44	nfel 2936	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵
119	1, 117, 118	nf3an 1933	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)
120	119, 20	nfim 1928	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))
121	50	eleq2d 2846	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵))
122	48, 121	3anbi23d 1467	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)))
123	122	imbi1d 344	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))))
124	120, 123, 21	chvarfv 2276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))
125	111, 116, 124	chvarfv 2276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
126	125	3adant1r 1196	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
127		simpr 490	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
128		simpl 488	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
129		simpl 488	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝑦 ∈ 𝐴)
130		simpr 490	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
131		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑗 / 𝑘⦌𝐶
132	44, 131	nfmpt 5202	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
133	2, 132	nffv 6895	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
134		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥+∞
135	133, 134	nfne 3058	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞
136		nfcv 2922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗𝐶
137	136, 109, 114	cbvmpt 5206	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
138	137	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
139	60, 138	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
140	139	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
141	140	neeq1d 3014	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
142	135, 141	rspc 3564	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
143	129, 130, 142	sylc 66	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)
144	127, 128, 143	syl2anc 596	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)
145	144	neneqd 2960	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)
146	145	adantll 727	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)
147	125	3expa 1136	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
148		eqid 2760	. . . . . . . . 9 ⊢ (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
149	147, 148	fmptd 7114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
150	149	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
151	102, 150	sge0repnf 47396	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ((Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞))
152	146, 151	mpbird 260	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ)
153	136, 109, 114	cbvmpt 5206	. . . . . . . . 9 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
154	104, 44, 50	cbviun 4992	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
155	154	mpteq1i 5195	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
156	153, 155	eqtri 2783	. . . . . . . 8 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
157	156	fveq2i 6888	. . . . . . 7 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
158	157, 28	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
159	158	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
160	69, 133, 140	cbvmpt 5206	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
161	160	fveq2i 6888	. . . . . . 7 ⊢ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))
162	11, 65	sge0cl 47391	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
163	162, 77	fmptd 7114	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
164	10, 163	sge0xrcl 47395	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
165	161, 164	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
166	165	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
167		eliun 4954	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
168	167	bilani 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
169		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
170		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑗
171		nfiu1 4985	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
172	170, 171	nfel 2936	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
173	169, 172	nfan 1931	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
174		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)
175	147	exp31 425	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
176	175	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
177	173, 174, 176	rexlimd 3269	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
178	168, 177	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
179		eqid 2760	. . . . . . 7 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
180	178, 179	fmptd 7114	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
181	180	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
182	154, 14	eqeltrrid 2865	. . . . . 6 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V)
183	182	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V)
184	95, 102, 107, 126, 152, 159, 166, 181, 183	sge0iunmptlemre 47425	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))))
185	157	a1i 11	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
186	161	a1i 11	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))))
187	184, 185, 186	3eqtr4d 2805	. . 3 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
188	88, 94, 187	syl2anc 596	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
189	87, 188	pm2.61dan 825	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⦋csb 3846 ⊆ wss 3895 ∪ ciun 4950 Disj wdisj 5069 class class class wbr 5102 ↦ cmpt 5185 ran crn 5651 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℝcr 11199 0cc0 11200 +∞cpnf 11340 ℝ^*cxr 11342 ≤ cle 11344 [,]cicc 13479 Σ^{^}csumge0 47372

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-xadd 13242 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-sum 15854 df-sumge0 47373

This theorem is used by: sge0iun 47429 sge0xp 47439

W3C validator