meaiuninclem - Mathbox for Glauco Siliprandi

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

Theorem meaiuninclem 42755

Description: Measures are continuous from below (bounded case): if 𝐸 is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)

**Hypotheses**
Ref	Expression
meaiuninclem.m	⊢ (𝜑 → 𝑀 ∈ Meas)
meaiuninclem.n	⊢ (𝜑 → 𝑁 ∈ ℤ)
meaiuninclem.z	⊢ 𝑍 = (ℤ_≥‘𝑁)
meaiuninclem.e	⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
meaiuninclem.i	⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))
meaiuninclem.b	⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
meaiuninclem.s	⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
meaiuninclem.f	⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))

**Assertion**
Ref	Expression
meaiuninclem	⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Distinct variable groups: 𝑖,𝐸,𝑛,𝑥 𝑖,𝐹,𝑛,𝑥 𝑖,𝑀,𝑛,𝑥 𝑖,𝑁,𝑛,𝑥 𝑆,𝑛,𝑥 𝑖,𝑍,𝑛,𝑥 𝜑,𝑖,𝑛,𝑥 Allowed substitution hint: 𝑆(𝑖)

Proof of Theorem meaiuninclem Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		meaiuninclem.z	. . 3 ⊢ 𝑍 = (ℤ_≥‘𝑁)
2		meaiuninclem.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℤ)
3		0xr 10682	. . . . . . 7 ⊢ 0 ∈ ℝ^*
4	3	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈ ℝ^*)
5		pnfxr 10689	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
6	5	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈ ℝ^*)
7		meaiuninclem.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ Meas)
8	7	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
9		eqid 2821	. . . . . . 7 ⊢ dom 𝑀 = dom 𝑀
10		meaiuninclem.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
11	10	ffvelrnda 6846	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
12	8, 9, 11	meaxrcl 42736	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
13	8, 11	meage0 42750	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐸‘𝑛)))
14		meaiuninclem.b	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
15	14	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
16		simp1 1132	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝜑 ∧ 𝑛 ∈ 𝑍))
17		simp2 1133	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ)
18		simp3 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
19	16	simprd 498	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑛 ∈ 𝑍)
20		rspa 3206	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
21	18, 19, 20	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
22	12	3ad2ant1 1129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
23		rexr 10681	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
24	23	3ad2ant2 1130	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ^*)
25	5	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈ ℝ^*)
26		simp3 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
27		ltpnf 12509	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
28	27	3ad2ant2 1130	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞)
29	22, 24, 25, 26, 28	xrlelttrd 12547	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
30	16, 17, 21, 29	syl3anc 1367	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
31	30	3exp 1115	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)))
32	31	rexlimdv 3283	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))
33	15, 32	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞)
34	4, 6, 12, 13, 33	elicod 12781	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞))
35		meaiuninclem.s	. . . . 5 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
36	34, 35	fmptd 6873	. . . 4 ⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞))
37		rge0ssre 12838	. . . . 5 ⊢ (0[,)+∞) ⊆ ℝ
38	37	a1i 11	. . . 4 ⊢ (𝜑 → (0[,)+∞) ⊆ ℝ)
39	36, 38	fssd 6523	. . 3 ⊢ (𝜑 → 𝑆:𝑍⟶ℝ)
40	1	peano2uzs 12296	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
41	40	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
42	10	ffvelrnda 6846	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
43	41, 42	syldan 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
44		meaiuninclem.i	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))
45	8, 9, 11, 43, 44	meassle 42738	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))
46	35	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
47		fvexd 6680	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V)
48	46, 47	fvmpt2d 6776	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛)))
49		2fveq3 6670	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚)))
50	49	cbvmptv 5162	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
51	35, 50	eqtri 2844	. . . . . 6 ⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
52		2fveq3 6670	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1))))
53		fvexd 6680	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V)
54	51, 52, 41, 53	fvmptd3 6786	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1))))
55	48, 54	breq12d 5072	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))))
56	45, 55	mpbird 259	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)))
57	48	eqcomd 2827	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛))
58	57	breq1d 5069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥))
59	58	ralbidva 3196	. . . . . . 7 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
60	59	biimpd 231	. . . . . 6 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
61	60	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
62	61	reximdva 3274	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
63	14, 62	mpd 15	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)
64	1, 2, 39, 56, 63	climsup 15020	. 2 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
65		nfv 1911	. . . . . 6 ⊢ Ⅎ𝑛𝜑
66		nfv 1911	. . . . . 6 ⊢ Ⅎ𝑥𝜑
67		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
68		fvex 6678	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑛) ∈ V
69	68	difexi 5225	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V)
71		meaiuninclem.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
72	71	fvmpt2 6774	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
73	67, 70, 72	syl2anc 586	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
74	73	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
75	7, 9	dmmeasal 42727	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
76	75	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
77		fzoct 41646	. . . . . . . . . . . 12 ⊢ (𝑁..^𝑛) ≼ ω
78	77	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω)
79	10	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀)
80		fzossuz 41642	. . . . . . . . . . . . . . . 16 ⊢ (𝑁..^𝑛) ⊆ (ℤ_≥‘𝑁)
81	1	eqcomi 2830	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑁) = 𝑍
82	80, 81	sseqtri 4003	. . . . . . . . . . . . . . 15 ⊢ (𝑁..^𝑛) ⊆ 𝑍
83	82	sseli 3963	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍)
84	83	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍)
85	79, 84	ffvelrnd 6847	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
86	85	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
87	76, 78, 86	saliuncl 42600	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀)
88		saldifcl2 42604	. . . . . . . . . 10 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
89	76, 11, 87, 88	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
90	74, 89	eqeltrd 2913	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀)
91	8, 9, 90	meaxrcl 42736	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ ℝ^*)
92	8, 90	meage0 42750	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛)))
93		difssd 4109	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛))
94	74, 93	eqsstrd 4005	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛))
95	8, 9, 90, 11, 94	meassle 42738	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛)))
96	91, 12, 6, 95, 33	xrlelttrd 12547	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞)
97	4, 6, 91, 92, 96	elicod 12781	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞))
98		2fveq3 6670	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖)))
99	98	breq1d 5069	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥))
100	99	cbvralvw 3450	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
101	100	biimpi 218	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
102	101	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
103		eleq1w 2895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍))
104	103	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍)))
105		oveq2 7158	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖))
106	105	sumeq1d 15052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
107	98, 106	eqeq12d 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))
108	104, 107	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))))
109		eleq1w 2895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍))
110	109	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍)))
111		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛))
112	111	iuneq1d 4939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
113	111	iuneq1d 4939	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
114	112, 113	eqeq12d 2837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))
115	110, 114	imbi12d 347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))))
116		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛))
117	116	cbviunv 4958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛))
119	65, 1, 10, 71	iundjiun 42735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
120	119	simplld 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
121	120	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
122		simpr 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍)
123		rspa 3206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
124	121, 122, 123	syl2anc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
125		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖))
126	125	cbviunv 4958	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
128	118, 124, 127	3eqtrd 2860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
129	115, 128	chvarvv 2001	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
130	67, 1	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑁))
131	130	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑁))
132		fvoveq1 7173	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1)))
133	125, 132	sseq12d 4000	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))
134	104, 133	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))))
135	134, 44	chvarvv 2001	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
136	84, 135	syldan 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
137	136	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
138	131, 137	iunincfi 41353	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛))
139	129, 138	eqtr2d 2857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
140	139	fveq2d 6669	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)))
141		nfv 1911	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍)
142		elfzuz 12898	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ_≥‘𝑁))
143	142, 81	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍)
144	143	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍)
145		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
146	145	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀))
147	104, 146	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)))
148	147, 90	chvarvv 2001	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)
149	144, 148	syldan 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
150	149	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
151		fzct 41640	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁...𝑛) ≼ ω
152	151	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω)
153	144	ssd 41337	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍)
154	119	simprd 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))
155	145	cbvdisjv 5035	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
156	154, 155	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
157		disjss1 5030	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁...𝑛) ⊆ 𝑍 → (Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)))
158	153, 156, 157	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
159	158	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
160	141, 8, 9, 150, 152, 159	meadjiun 42741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) = (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))))
161		fzfid 13335	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin)
162		2fveq3 6670	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖)))
163	162	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))
164	104, 163	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))))
165	164, 97	chvarvv 2001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
166	144, 165	syldan 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
167	166	adantlr 713	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
168	161, 167	sge0fsummpt 42665	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)))
169		2fveq3 6670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚)))
170	169	cbvsumv 15047	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))
171	170	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
172	168, 171	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
173	140, 160, 172	3eqtrd 2860	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
174	108, 173	chvarvv 2001	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
175		2fveq3 6670	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛)))
176	175	cbvsumv 15047	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))
177	176	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
178	174, 177	eqtrd 2856	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
179	178	breq1d 5069	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
180	179	ralbidva 3196	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
181	180	biimpd 231	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
182	181	imp 409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
183	102, 182	syldan 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
184	183	ex 415	. . . . . . . 8 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
185	184	reximdv 3273	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
186	14, 185	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
187	65, 66, 2, 1, 97, 186	sge0reuzb 42723	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
188	98	cbvmptv 5162	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
189	35, 188	eqtri 2844	. . . . . . . . 9 ⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
190	189	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))))
191	178	mpteq2dva 5154	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
192	190, 191	eqtrd 2856	. . . . . . 7 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
193	192	rneqd 5803	. . . . . 6 ⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
194	193	supeq1d 8904	. . . . 5 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
195	187, 194	eqtr4d 2859	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < ))
196	195	eqcomd 2827	. . 3 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
197	1	uzct 41318	. . . . . 6 ⊢ 𝑍 ≼ ω
198	197	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑍 ≼ ω)
199	65, 7, 9, 90, 198, 154	meadjiun 42741	. . . 4 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
200	199	eqcomd 2827	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
201	119	simplrd 768	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
202	201	fveq2d 6669	. . 3 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
203	196, 200, 202	3eqtrd 2860	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
204	64, 203	breqtrd 5085	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 Vcvv 3495 ∖ cdif 3933 ⊆ wss 3936 ∪ ciun 4912 Disj wdisj 5024 class class class wbr 5059 ↦ cmpt 5139 dom cdm 5550 ran crn 5551 ⟶wf 6346 ‘cfv 6350 (class class class)co 7150 ωcom 7574 ≼ cdom 8501 supcsup 8898 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 +∞cpnf 10666 ℝ^*cxr 10668 < clt 10669 ≤ cle 10670 ℤcz 11975 ℤ_≥cuz 12237 [,)cico 12734 ...cfz 12886 ..^cfzo 13027 ⇝ cli 14835 Σcsu 15036 SAlgcsalg 42586 Σ^{^}csumge0 42637 Meascmea 42724

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-disj 5025 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-se 5510 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-isom 6359 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-omul 8101 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-oi 8968 df-card 9362 df-acn 9365 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-xadd 12502 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-clim 14839 df-sum 15037 df-salg 42587 df-sumge0 42638 df-mea 42725

This theorem is referenced by: meaiuninc 42756

W3C validator