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 46409

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 1914	. . . 4 ⊢ Ⅎ𝑥𝜑
2		nfcv 2891	. . . . . 6 ⊢ Ⅎ𝑥Σ^{^}
3		nfiu1 4987	. . . . . . 7 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
5	3, 4	nfmpt 5200	. . . . . 6 ⊢ Ⅎ𝑥(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
6	2, 5	nffv 6850	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))
7		nfmpt1 5201	. . . . . 6 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
8	2, 7	nffv 6850	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
9	6, 8	nfeq 2905	. . . 4 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
10		sge0iunmpt.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
11		sge0iunmpt.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
12	11	ralrimiva 3125	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
13		iunexg 7921	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
14	10, 12, 13	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
15		eliun 4955	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
16	15	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
17	16	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
18		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑘
19	18, 3	nfel 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
20	1, 19	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
21	4	nfel1 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,]+∞)
22		sge0iunmpt.c	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
23	22	3exp 1119	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
25	20, 21, 24	rexlimd 3242	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
26	17, 25	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
27		eqid 2729	. . . . . . . . . 10 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
28	26, 27	fmptd 7068	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
29	14, 28	sge0xrcl 46376	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
30	29	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
31		id 22	. . . . . . . . . . 11 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
32	31	eqcomd 2735	. . . . . . . . . 10 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
33	32	adantl 481	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
34	33	3adant1 1130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
35	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
36	26	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
37		ssiun2 5006	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	37	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
39	35, 36, 38	sge0lessmpt 46390	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
40	39	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
41	34, 40	eqbrtrd 5124	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
42	30, 41	xrgepnfd 45320	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞)
43	10	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉)
44		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴)
45		nfcsb1v 3883	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
46		nfcsb1v 3883	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊
47	45, 46	nfel 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊
48	44, 47	nfim 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
49		eleq1w 2811	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
50	49	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴)))
51		csbeq1a 3873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
52		csbeq1a 3873	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝑊 = ⦋𝑦 / 𝑥⦌𝑊)
53	51, 52	eleq12d 2822	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊))
54	50, 53	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)))
55	48, 54, 11	chvarfv 2241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
56	55	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
57	45, 4	nfmpt 5200	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)
58		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(0[,]+∞)
59	57, 45, 58	nff 6666	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)
60	44, 59	nfim 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
61	51	mpteq1d 5192	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
62	61, 51	feq12d 6658	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)))
63	50, 62	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))))
64	23	imp31 417	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
65		eqid 2729	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
66	64, 65	fmptd 7068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
67	60, 63, 66	chvarfv 2241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
68	67	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
69	56, 68	sge0cl 46372	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
70		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑦(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))
71	2, 57	nffv 6850	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
72	61	fveq2d 6844	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
73	70, 71, 72	cbvmpt 5204	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
74	69, 73	fmptd 7068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
75	74	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
76		id 22	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
77		fvexd 6855	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V)
78		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
79	78	elrnmpt1 5913	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
80	76, 77, 79	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
81	80	adantr 480	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
82	33, 81	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
83	82	3adant1 1130	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
84	43, 75, 83	sge0pnfval 46364	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞)
85	42, 84	eqtr4d 2767	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
86	85	3exp 1119	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))))
87	1, 9, 86	rexlimd 3242	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
88	87	imp 406	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
89		simpl 482	. . 3 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝜑)
90		ralnex 3055	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
91		df-ne 2926	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
92	91	bicomi 224	. . . . . 6 ⊢ (¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
93	92	ralbii 3075	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
94	90, 93	sylbb1 237	. . . 4 ⊢ (¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
95	94	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
96	10	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝐴 ∈ 𝑉)
97		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑊
98	45, 97	nfel 2906	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊
99	44, 98	nfim 1896	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
100	51	eleq1d 2813	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊))
101	50, 100	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)))
102	99, 101, 11	chvarfv 2241	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
103	102	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
104		sge0iunmpt.dj	. . . . . . 7 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
105		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
106	105, 45, 51	cbvdisj 5079	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
107	104, 106	sylib 218	. . . . . 6 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
108	107	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
109		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
110		nfcsb1v 3883	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶
111	110	nfel1 2908	. . . . . . . 8 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)
112	109, 111	nfim 1896	. . . . . . 7 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
113		eleq1w 2811	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵))
114	113	3anbi3d 1444	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)))
115		csbeq1a 3873	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑘⦌𝐶)
116	115	eleq1d 2813	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔ ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
117	114, 116	imbi12d 344	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
118		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
119	18, 45	nfel 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵
120	1, 118, 119	nf3an 1901	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)
121	120, 21	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))
122	51	eleq2d 2814	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵))
123	49, 122	3anbi23d 1441	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)))
124	123	imbi1d 341	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))))
125	121, 124, 22	chvarfv 2241	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))
126	112, 117, 125	chvarfv 2241	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
127	126	3adant1r 1178	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
128		simpr 484	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
129		simpl 482	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
130		simpl 482	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝑦 ∈ 𝐴)
131		simpr 484	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
132		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑗 / 𝑘⦌𝐶
133	45, 132	nfmpt 5200	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
134	2, 133	nffv 6850	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
135		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥+∞
136	134, 135	nfne 3026	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞
137		nfcv 2891	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗𝐶
138	137, 110, 115	cbvmpt 5204	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
139	138	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
140	61, 139	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
141	140	fveq2d 6844	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
142	141	neeq1d 2984	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
143	136, 142	rspc 3573	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
144	130, 131, 143	sylc 65	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)
145	128, 129, 144	syl2anc 584	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)
146	145	neneqd 2930	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)
147	146	adantll 714	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)
148	126	3expa 1118	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
149		eqid 2729	. . . . . . . . 9 ⊢ (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
150	148, 149	fmptd 7068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
151	150	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
152	103, 151	sge0repnf 46377	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ((Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞))
153	147, 152	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ)
154	137, 110, 115	cbvmpt 5204	. . . . . . . . 9 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
155	105, 45, 51	cbviun 4995	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
156	155	mpteq1i 5193	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
157	154, 156	eqtri 2752	. . . . . . . 8 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
158	157	fveq2i 6843	. . . . . . 7 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
159	158, 29	eqeltrrid 2833	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
160	159	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
161	70, 134, 141	cbvmpt 5204	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
162	161	fveq2i 6843	. . . . . . 7 ⊢ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))
163	11, 66	sge0cl 46372	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
164	163, 78	fmptd 7068	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
165	10, 164	sge0xrcl 46376	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
166	162, 165	eqeltrrid 2833	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
167	166	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
168		eliun 4955	. . . . . . . . . 10 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
169	168	biimpi 216	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
170	169	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
171		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
172		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑗
173		nfiu1 4987	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
174	172, 173	nfel 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
175	171, 174	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
176		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)
177	148	exp31 419	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
178	177	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
179	175, 176, 178	rexlimd 3242	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
180	170, 179	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
181		eqid 2729	. . . . . . 7 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
182	180, 181	fmptd 7068	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
183	182	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
184	155, 14	eqeltrrid 2833	. . . . . 6 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V)
185	184	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V)
186	96, 103, 108, 127, 153, 160, 167, 183, 185	sge0iunmptlemre 46406	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))))
187	158	a1i 11	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
188	162	a1i 11	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))))
189	186, 187, 188	3eqtr4d 2774	. . 3 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
190	89, 95, 189	syl2anc 584	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
191	88, 190	pm2.61dan 812	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 Vcvv 3444 ⦋csb 3859 ⊆ wss 3911 ∪ ciun 4951 Disj wdisj 5069 class class class wbr 5102 ↦ cmpt 5183 ran crn 5632 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 ℝcr 11043 0cc0 11044 +∞cpnf 11181 ℝ^*cxr 11183 ≤ cle 11185 [,]cicc 13285 Σ^{^}csumge0 46353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-ac2 10392 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-disj 5070 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-oi 9439 df-card 9868 df-acn 9871 df-ac 10045 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-rp 12928 df-xadd 13049 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629 df-sumge0 46354

This theorem is referenced by: sge0iun 46410 sge0xp 46420

W3C validator