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 46577

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 11159	. . . . . . 7 ⊢ 0 ∈ ℝ^*
4	3	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈ ℝ^*)
5		pnfxr 11166	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
6	5	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈ ℝ^*)
7		meaiuninclem.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ Meas)
8	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
9		eqid 2731	. . . . . . 7 ⊢ dom 𝑀 = dom 𝑀
10		meaiuninclem.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
11	10	ffvelcdmda 7017	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
12	8, 9, 11	meaxrcl 46558	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
13	8, 11	meage0 46572	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐸‘𝑛)))
14		meaiuninclem.b	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
15	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
16		simp1 1136	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝜑 ∧ 𝑛 ∈ 𝑍))
17		simp2 1137	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ)
18		simp3 1138	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
19	16	simprd 495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑛 ∈ 𝑍)
20		rspa 3221	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
21	18, 19, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
22	12	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
23		rexr 11158	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
24	23	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ^*)
25	5	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈ ℝ^*)
26		simp3 1138	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
27		ltpnf 13019	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
28	27	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞)
29	22, 24, 25, 26, 28	xrlelttrd 13059	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
30	16, 17, 21, 29	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
31	30	3exp 1119	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)))
32	31	rexlimdv 3131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))
33	15, 32	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞)
34	4, 6, 12, 13, 33	elicod 13295	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞))
35		meaiuninclem.s	. . . . 5 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
36	34, 35	fmptd 7047	. . . 4 ⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞))
37		rge0ssre 13356	. . . . 5 ⊢ (0[,)+∞) ⊆ ℝ
38	37	a1i 11	. . . 4 ⊢ (𝜑 → (0[,)+∞) ⊆ ℝ)
39	36, 38	fssd 6668	. . 3 ⊢ (𝜑 → 𝑆:𝑍⟶ℝ)
40	1	peano2uzs 12800	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
41	40	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
42	10	ffvelcdmda 7017	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
43	41, 42	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
44		meaiuninclem.i	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))
45	8, 9, 11, 43, 44	meassle 46560	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))
46	35	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
47		fvexd 6837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V)
48	46, 47	fvmpt2d 6942	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛)))
49		2fveq3 6827	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚)))
50	49	cbvmptv 5193	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
51	35, 50	eqtri 2754	. . . . . 6 ⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
52		2fveq3 6827	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1))))
53		fvexd 6837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V)
54	51, 52, 41, 53	fvmptd3 6952	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1))))
55	48, 54	breq12d 5102	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))))
56	45, 55	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)))
57	48	eqcomd 2737	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛))
58	57	breq1d 5099	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥))
59	58	ralbidva 3153	. . . . . . 7 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
60	59	biimpd 229	. . . . . 6 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
61	60	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
62	61	reximdva 3145	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
63	14, 62	mpd 15	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)
64	1, 2, 39, 56, 63	climsup 15577	. 2 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
65		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑛𝜑
66		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑥𝜑
67		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
68		fvex 6835	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑛) ∈ V
69	68	difexi 5266	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V)
71		meaiuninclem.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
72	71	fvmpt2 6940	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
73	67, 70, 72	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
74	73	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
75	7, 9	dmmeasal 46549	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
76	75	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
77		fzoct 45481	. . . . . . . . . . . 12 ⊢ (𝑁..^𝑛) ≼ ω
78	77	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω)
79	10	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀)
80		fzossuz 45478	. . . . . . . . . . . . . . . 16 ⊢ (𝑁..^𝑛) ⊆ (ℤ_≥‘𝑁)
81	1	eqcomi 2740	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑁) = 𝑍
82	80, 81	sseqtri 3978	. . . . . . . . . . . . . . 15 ⊢ (𝑁..^𝑛) ⊆ 𝑍
83	82	sseli 3925	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍)
84	83	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍)
85	79, 84	ffvelcdmd 7018	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
86	85	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
87	76, 78, 86	saliuncl 46420	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀)
88		saldifcl2 46425	. . . . . . . . . 10 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
89	76, 11, 87, 88	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
90	74, 89	eqeltrd 2831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀)
91	8, 9, 90	meaxrcl 46558	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ ℝ^*)
92	8, 90	meage0 46572	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛)))
93		difssd 4084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛))
94	74, 93	eqsstrd 3964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛))
95	8, 9, 90, 11, 94	meassle 46560	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛)))
96	91, 12, 6, 95, 33	xrlelttrd 13059	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞)
97	4, 6, 91, 92, 96	elicod 13295	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞))
98		2fveq3 6827	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖)))
99	98	breq1d 5099	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥))
100	99	cbvralvw 3210	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
101	100	biimpi 216	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
102	101	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
103		eleq1w 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍))
104	103	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍)))
105		oveq2 7354	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖))
106	105	sumeq1d 15607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
107	98, 106	eqeq12d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))
108	104, 107	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))))
109		eleq1w 2814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍))
110	109	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍)))
111		oveq2 7354	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛))
112	111	iuneq1d 4967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
113	111	iuneq1d 4967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
114	112, 113	eqeq12d 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))
115	110, 114	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))))
116		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛))
117	116	cbviunv 4987	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛))
119	65, 1, 10, 71	iundjiun 46557	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
120	119	simplld 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
121	120	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
122		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍)
123		rspa 3221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
124	121, 122, 123	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
125		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖))
126	125	cbviunv 4987	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
128	118, 124, 127	3eqtrd 2770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
129	115, 128	chvarvv 1990	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
130	67, 1	eleqtrdi 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑁))
131	130	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑁))
132		fvoveq1 7369	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1)))
133	125, 132	sseq12d 3963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))
134	104, 133	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))))
135	134, 44	chvarvv 1990	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
136	84, 135	syldan 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
137	136	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
138	131, 137	iunincfi 45190	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛))
139	129, 138	eqtr2d 2767	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
140	139	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)))
141		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍)
142		elfzuz 13420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ_≥‘𝑁))
143	142, 81	eleqtrdi 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍)
145		fveq2 6822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
146	145	eleq1d 2816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀))
147	104, 146	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)))
148	147, 90	chvarvv 1990	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)
149	144, 148	syldan 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
150	149	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
151		fzct 45476	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁...𝑛) ≼ ω
152	151	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω)
153	144	ssd 45176	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍)
154	119	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))
155	145	cbvdisjv 5067	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
156	154, 155	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
157		disjss1 5062	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁...𝑛) ⊆ 𝑍 → (Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)))
158	153, 156, 157	sylc 65	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
159	158	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
160	141, 8, 9, 150, 152, 159	meadjiun 46563	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) = (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))))
161		fzfid 13880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin)
162		2fveq3 6827	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖)))
163	162	eleq1d 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))
164	104, 163	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))))
165	164, 97	chvarvv 1990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
166	144, 165	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
167	166	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
168	161, 167	sge0fsummpt 46487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)))
169		2fveq3 6827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚)))
170	169	cbvsumv 15603	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))
171	170	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
172	168, 171	eqtrd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
173	140, 160, 172	3eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
174	108, 173	chvarvv 1990	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
175		2fveq3 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛)))
176	175	cbvsumv 15603	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))
177	176	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
178	174, 177	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
179	178	breq1d 5099	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
180	179	ralbidva 3153	. . . . . . . . . . . 12 ⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
181	180	biimpd 229	. . . . . . . . . . 11 ⊢ (𝜑 → (∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
182	181	imp 406	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
183	102, 182	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
184	183	ex 412	. . . . . . . 8 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
185	184	reximdv 3147	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
186	14, 185	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
187	65, 66, 2, 1, 97, 186	sge0reuzb 46545	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
188	98	cbvmptv 5193	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
189	35, 188	eqtri 2754	. . . . . . . . 9 ⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
190	189	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))))
191	178	mpteq2dva 5182	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
192	190, 191	eqtrd 2766	. . . . . . 7 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
193	192	rneqd 5877	. . . . . 6 ⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
194	193	supeq1d 9330	. . . . 5 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
195	187, 194	eqtr4d 2769	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < ))
196	195	eqcomd 2737	. . 3 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
197	1	uzct 45159	. . . . . 6 ⊢ 𝑍 ≼ ω
198	197	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑍 ≼ ω)
199	65, 7, 9, 90, 198, 154	meadjiun 46563	. . . 4 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
200	199	eqcomd 2737	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
201	119	simplrd 769	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
202	201	fveq2d 6826	. . 3 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
203	196, 200, 202	3eqtrd 2770	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
204	64, 203	breqtrd 5115	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 Vcvv 3436 ∖ cdif 3894 ⊆ wss 3897 ∪ ciun 4939 Disj wdisj 5056 class class class wbr 5089 ↦ cmpt 5170 dom cdm 5614 ran crn 5615 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ωcom 7796 ≼ cdom 8867 supcsup 9324 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 +∞cpnf 11143 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 ℤcz 12468 ℤ_≥cuz 12732 [,)cico 13247 ...cfz 13407 ..^cfzo 13554 ⇝ cli 15391 Σcsu 15593 SAlgcsalg 46405 Σ^{^}csumge0 46459 Meascmea 46546

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-disj 5057 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-oadd 8389 df-omul 8390 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-oi 9396 df-card 9832 df-acn 9835 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-xadd 13012 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594 df-salg 46406 df-sumge0 46460 df-mea 46547

This theorem is referenced by: meaiuninc 46578

W3C validator