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 46416

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 4991	. . . . . . 7 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
4		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑥𝐶
5	3, 4	nfmpt 5205	. . . . . 6 ⊢ Ⅎ𝑥(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
6	2, 5	nffv 6868	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))
7		nfmpt1 5206	. . . . . 6 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
8	2, 7	nffv 6868	. . . . 5 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
9	6, 8	nfeq 2905	. . . 4 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
10		sge0iunmpt.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
11		sge0iunmpt.b	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
12	11	ralrimiva 3125	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊)
13		iunexg 7942	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
14	10, 12, 13	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
15		eliun 4959	. . . . . . . . . . . . 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 3244	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,]+∞)))
26	17, 25	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
27		eqid 2729	. . . . . . . . . 10 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)
28	26, 27	fmptd 7086	. . . . . . . . 9 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
29	14, 28	sge0xrcl 46383	. . . . . . . 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 5011	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	37	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
39	35, 36, 38	sge0lessmpt 46397	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
40	39	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
41	34, 40	eqbrtrd 5129	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → +∞ ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
42	30, 41	xrgepnfd 45327	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = +∞)
43	10	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → 𝐴 ∈ 𝑉)
44		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ 𝐴)
45		nfcsb1v 3886	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵
46		nfcsb1v 3886	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝑊
47	45, 46	nfel 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊
48	44, 47	nfim 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → ⦋𝑦 / 𝑥⦌𝐵 ∈ ⦋𝑦 / 𝑥⦌𝑊)
49		eleq1w 2811	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
50	49	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑦 ∈ 𝐴)))
51		csbeq1a 3876	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵)
52		csbeq1a 3876	. . . . . . . . . . . . . 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 5205	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)
58		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(0[,]+∞)
59	57, 45, 58	nff 6684	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞)
60	44, 59	nfim 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
61	51	mpteq1d 5197	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
62	61, 51	feq12d 6676	. . . . . . . . . . . . 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 7086	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
67	60, 63, 66	chvarfv 2241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
68	67	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
69	56, 68	sge0cl 46379	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
70		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑦(Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))
71	2, 57	nffv 6868	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶))
72	61	fveq2d 6862	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
73	70, 71, 72	cbvmpt 5209	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶)))
74	69, 73	fmptd 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
75	74	3adant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
76		id 22	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
77		fvexd 6873	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ V)
78		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
79	78	elrnmpt1 5924	. . . . . . . . . . 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 46371	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = +∞)
85	42, 84	eqtr4d 2767	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
86	85	3exp 1119	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = +∞ → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))))
87	1, 9, 86	rexlimd 3244	. . 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 5084	. . . . . . 7 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
107	104, 106	sylib 218	. . . . . 6 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
108	107	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → Disj 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵)
109		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
110		nfcsb1v 3886	. . . . . . . . 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 3876	. . . . . . . . 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 5205	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
134	2, 133	nffv 6868	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
135		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥+∞
136	134, 135	nfne 3026	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞
137		nfcv 2891	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗𝐶
138	137, 110, 115	cbvmpt 5209	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
139	138	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
140	61, 139	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
141	140	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
142	141	neeq1d 2984	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞ ↔ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ≠ +∞))
143	136, 142	rspc 3576	. . . . . . . . . 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 7086	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
151	150	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶):⦋𝑦 / 𝑥⦌𝐵⟶(0[,]+∞))
152	103, 151	sge0repnf 46384	. . . . . 6 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → ((Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ ↔ ¬ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) = +∞))
153	147, 152	mpbird 257	. . . . 5 ⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) ∧ 𝑦 ∈ 𝐴) → (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ)
154	137, 110, 115	cbvmpt 5209	. . . . . . . . 9 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
155	105, 45, 51	cbviun 5000	. . . . . . . . . 10 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵
156	155	mpteq1i 5198	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
157	154, 156	eqtri 2752	. . . . . . . 8 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
158	157	fveq2i 6861	. . . . . . 7 ⊢ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))
159	158, 29	eqeltrrid 2833	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
160	159	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)) ∈ ℝ^*)
161	70, 134, 141	cbvmpt 5209	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))
162	161	fveq2i 6861	. . . . . . 7 ⊢ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶))))
163	11, 66	sge0cl 46379	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
164	163, 78	fmptd 7086	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
165	10, 164	sge0xrcl 46383	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
166	162, 165	eqeltrrid 2833	. . . . . 6 ⊢ (𝜑 → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
167	166	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≠ +∞) → (Σ^{^}‘(𝑦 ∈ 𝐴 ↦ (Σ^{^}‘(𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)))) ∈ ℝ^*)
168		eliun 4959	. . . . . . . . . 10 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
169	168	biimpi 216	. . . . . . . . 9 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
170	169	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵)
171		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
172		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑗
173		nfiu1 4991	. . . . . . . . . . 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 3244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → (∃𝑦 ∈ 𝐴 𝑗 ∈ ⦋𝑦 / 𝑥⦌𝐵 → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞)))
180	170, 179	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵) → ⦋𝑗 / 𝑘⦌𝐶 ∈ (0[,]+∞))
181		eqid 2729	. . . . . . 7 ⊢ (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶) = (𝑗 ∈ ∪ 𝑦 ∈ 𝐴 ⦋𝑦 / 𝑥⦌𝐵 ↦ ⦋𝑗 / 𝑘⦌𝐶)
182	180, 181	fmptd 7086	. . . . . 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 46413	. . . 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 3447 ⦋csb 3862 ⊆ wss 3914 ∪ ciun 4955 Disj wdisj 5074 class class class wbr 5107 ↦ cmpt 5188 ran crn 5639 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 ℝcr 11067 0cc0 11068 +∞cpnf 11205 ℝ^*cxr 11207 ≤ cle 11209 [,]cicc 13309 Σ^{^}csumge0 46360

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 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-ac2 10416 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

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 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-disj 5075 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-map 8801 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-oi 9463 df-card 9892 df-acn 9895 df-ac 10069 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-z 12530 df-uz 12794 df-rp 12952 df-xadd 13073 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-sum 15653 df-sumge0 46361

This theorem is referenced by: sge0iun 46417 sge0xp 46427

W3C validator