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 46843

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 1916	. . . 4 ⊢ Ⅎ𝑥𝜑
2		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑥Σ^{^}
3		nfiu1 4970	. . . . . . 7 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
5	3, 4	nfmpt 5184	. . . . . 6 ⊢ Ⅎ𝑥(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
6	2, 5	nffv 6848	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))
7		nfmpt1 5185	. . . . . 6 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
8	2, 7	nffv 6848	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
9	6, 8	nfeq 2913	. . . 4 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
10		sge0iunmpt.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
11		sge0iunmpt.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
12	11	ralrimiva 3130	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
13		iunexg 7913	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
14	10, 12, 13	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
15		eliun 4938	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
16	15	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
17	16	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
18		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝑘
19	18, 3	nfel 2914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
20	1, 19	nfan 1901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
21	4	nfel1 2916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,]+∞)
22		sge0iunmpt.c	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
23	22	3exp 1120	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞))))
25	20, 21, 24	rexlimd 3245	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
26	17, 25	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
27		eqid 2737	. . . . . . . . . 10 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
28	26, 27	fmptd 7064	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
29	14, 28	sge0xrcl 46810	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
30	29	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
31		id 22	. . . . . . . . . . 11 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
32	31	eqcomd 2743	. . . . . . . . . 10 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
33	32	adantl 481	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
34	33	3adant1 1131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ = (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
35	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
36	26	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
37		ssiun2 4991	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	37	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
39	35, 36, 38	sge0lessmpt 46824	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
40	39	3adant3 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
41	34, 40	eqbrtrd 5108	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
42	30, 41	xrgepnfd 45758	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞)
43	10	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉)
44		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴)
45		nfcsb1v 3862	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
46		nfcsb1v 3862	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊
47	45, 46	nfel 2914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊
48	44, 47	nfim 1898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
49		eleq1w 2820	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
50	49	anbi2d 631	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴)))
51		csbeq1a 3852	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
52		csbeq1a 3852	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝑊 = ⦋𝑦 / 𝑥⦌𝑊)
53	51, 52	eleq12d 2831	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊))
54	50, 53	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)))
55	48, 54, 11	chvarfv 2248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
56	55	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
57	45, 4	nfmpt 5184	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)
58		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(0[,]+∞)
59	57, 45, 58	nff 6662	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)
60	44, 59	nfim 1898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
61	51	mpteq1d 5176	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
62	61, 51	feq12d 6654	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)))
63	50, 62	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))))
64	23	imp31 417	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
65		eqid 2737	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
66	64, 65	fmptd 7064	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
67	60, 63, 66	chvarfv 2248	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
68	67	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
69	56, 68	sge0cl 46806	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
70		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑦(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))
71	2, 57	nffv 6848	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
72	61	fveq2d 6842	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
73	70, 71, 72	cbvmpt 5188	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
74	69, 73	fmptd 7064	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
75	74	3adant3 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
76		id 22	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
77		fvexd 6853	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V)
78		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
79	78	elrnmpt1 5913	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
80	76, 77, 79	syl2anc 585	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
81	80	adantr 480	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
82	33, 81	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
83	82	3adant1 1131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ∈ ran (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
84	43, 75, 83	sge0pnfval 46798	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞)
85	42, 84	eqtr4d 2775	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
86	85	3exp 1120	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))))
87	1, 9, 86	rexlimd 3245	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
88	87	imp 406	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
89		simpl 482	. . 3 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝜑)
90		ralnex 3064	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
91		df-ne 2934	. . . . . . 7 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞)
92	91	bicomi 224	. . . . . 6 ⊢ (¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
93	92	ralbii 3084	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ¬ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ ↔ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
94	90, 93	sylbb1 237	. . . 4 ⊢ (¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
95	94	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
96	10	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝐴 ∈ 𝑉)
97		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑊
98	45, 97	nfel 2914	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊
99	44, 98	nfim 1898	. . . . . . 7 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
100	51	eleq1d 2822	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑊 ↔ ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊))
101	50, 100	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)))
102	99, 101, 11	chvarfv 2248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
103	102	adantlr 716	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ 𝑊)
104		sge0iunmpt.dj	. . . . . . 7 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
105		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
106	105, 45, 51	cbvdisj 5063	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
107	104, 106	sylib 218	. . . . . 6 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
108	107	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
109		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
110		nfcsb1v 3862	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶
111	110	nfel1 2916	. . . . . . . 8 ⊢ Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)
112	109, 111	nfim 1898	. . . . . . 7 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
113		eleq1w 2820	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↔ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵))
114	113	3anbi3d 1445	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)))
115		csbeq1a 3852	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → 𝐶 = ⦋𝑗 / 𝑘⦌𝐶)
116	115	eleq1d 2822	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔ ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
117	114, 116	imbi12d 344	. . . . . . 7 ⊢ (𝑘 = 𝑗 → (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
118		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
119	18, 45	nfel 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵
120	1, 118, 119	nf3an 1903	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)
121	120, 21	nfim 1898	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))
122	51	eleq2d 2823	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵))
123	49, 122	3anbi23d 1442	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵)))
124	123	imbi1d 341	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))))
125	121, 124, 22	chvarfv 2248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,]+∞))
126	112, 117, 125	chvarfv 2248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
127	126	3adant1r 1179	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
128		simpr 484	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
129		simpl 482	. . . . . . . . 9 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
130		simpl 482	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → 𝑦 ∈ 𝐴)
131		simpr 484	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞)
132		nfcv 2899	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑗 / 𝑘⦌𝐶
133	45, 132	nfmpt 5184	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
134	2, 133	nffv 6848	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
135		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥+∞
136	134, 135	nfne 3034	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞
137		nfcv 2899	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗𝐶
138	137, 110, 115	cbvmpt 5188	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
139	138	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
140	61, 139	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
141	140	fveq2d 6842	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
142	141	neeq1d 2992	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
143	136, 142	rspc 3553	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
144	130, 131, 143	sylc 65	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)
145	128, 129, 144	syl2anc 585	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞)
146	145	neneqd 2938	. . . . . . 7 ⊢ ((∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ∧ 𝑦 ∈ 𝐴) → ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)
147	146	adantll 715	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞)
148	126	3expa 1119	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
149		eqid 2737	. . . . . . . . 9 ⊢ (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
150	148, 149	fmptd 7064	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
151	150	adantlr 716	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
152	103, 151	sge0repnf 46811	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ((Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞))
153	147, 152	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ)
154	137, 110, 115	cbvmpt 5188	. . . . . . . . 9 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
155	105, 45, 51	cbviun 4978	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
156	155	mpteq1i 5177	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
157	154, 156	eqtri 2760	. . . . . . . 8 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
158	157	fveq2i 6841	. . . . . . 7 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
159	158, 29	eqeltrrid 2842	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
160	159	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
161	70, 134, 141	cbvmpt 5188	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
162	161	fveq2i 6841	. . . . . . 7 ⊢ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))
163	11, 66	sge0cl 46806	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
164	163, 78	fmptd 7064	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
165	10, 164	sge0xrcl 46810	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
166	162, 165	eqeltrrid 2842	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
167	166	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
168		eliun 4938	. . . . . . . . . 10 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
169	168	biimpi 216	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
170	169	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
171		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
172		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑗
173		nfiu1 4970	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
174	172, 173	nfel 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑦 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
175	171, 174	nfan 1901	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
176		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)
177	148	exp31 419	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
178	177	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (𝑦 ∈ 𝐴 → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))))
179	175, 176, 178	rexlimd 3245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
180	170, 179	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
181		eqid 2737	. . . . . . 7 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
182	180, 181	fmptd 7064	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
183	182	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
184	155, 14	eqeltrrid 2842	. . . . . 6 ⊢ (𝜑 → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V)
185	184	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ∈ V)
186	96, 103, 108, 127, 153, 160, 167, 183, 185	sge0iunmptlemre 46840	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))))
187	158	a1i 11	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
188	162	a1i 11	. . . 4 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))))
189	186, 187, 188	3eqtr4d 2782	. . 3 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
190	89, 95, 189	syl2anc 585	. 2 ⊢ ((𝜑 ∧ ¬ ∃𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
191	88, 190	pm2.61dan 813	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ⦋csb 3838 ⊆ wss 3890 ∪ ciun 4934 Disj wdisj 5053 class class class wbr 5086 ↦ cmpt 5167 ran crn 5629 ⟶wf 6492 ‘cfv 6496 (class class class)co 7364 ℝcr 11034 0cc0 11035 +∞cpnf 11173 ℝ^*cxr 11175 ≤ cle 11177 [,]cicc 13298 Σ^{^}csumge0 46787

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 5306 ax-pr 5374 ax-un 7686 ax-inf2 9559 ax-ac2 10382 ax-cnex 11091 ax-resscn 11092 ax-1cn 11093 ax-icn 11094 ax-addcl 11095 ax-addrcl 11096 ax-mulcl 11097 ax-mulrcl 11098 ax-mulcom 11099 ax-addass 11100 ax-mulass 11101 ax-distr 11102 ax-i2m1 11103 ax-1ne0 11104 ax-1rid 11105 ax-rnegex 11106 ax-rrecex 11107 ax-cnre 11108 ax-pre-lttri 11109 ax-pre-lttrn 11110 ax-pre-ltadd 11111 ax-pre-mulgt0 11112 ax-pre-sup 11113

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 5523 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5581 df-se 5582 df-we 5583 df-xp 5634 df-rel 5635 df-cnv 5636 df-co 5637 df-dm 5638 df-rn 5639 df-res 5640 df-ima 5641 df-pred 6263 df-ord 6324 df-on 6325 df-lim 6326 df-suc 6327 df-iota 6452 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7321 df-ov 7367 df-oprab 7368 df-mpo 7369 df-om 7815 df-1st 7939 df-2nd 7940 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-er 8640 df-map 8772 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-sup 9352 df-oi 9422 df-card 9860 df-acn 9863 df-ac 10035 df-pnf 11178 df-mnf 11179 df-xr 11180 df-ltxr 11181 df-le 11182 df-sub 11376 df-neg 11377 df-div 11805 df-nn 12172 df-2 12241 df-3 12242 df-n0 12435 df-z 12522 df-uz 12786 df-rp 12940 df-xadd 13061 df-ico 13301 df-icc 13302 df-fz 13459 df-fzo 13606 df-seq 13961 df-exp 14021 df-hash 14290 df-cj 15058 df-re 15059 df-im 15060 df-sqrt 15194 df-abs 15195 df-clim 15447 df-sum 15646 df-sumge0 46788

This theorem is referenced by: sge0iun 46844 sge0xp 46854

W3C validator