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 46495

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 11308	. . . . . . 7 ⊢ 0 ∈ ℝ^*
4	3	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈ ℝ^*)
5		pnfxr 11315	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
6	5	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈ ℝ^*)
7		meaiuninclem.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ Meas)
8	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
9		eqid 2737	. . . . . . 7 ⊢ dom 𝑀 = dom 𝑀
10		meaiuninclem.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
11	10	ffvelcdmda 7104	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
12	8, 9, 11	meaxrcl 46476	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
13	8, 11	meage0 46490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐸‘𝑛)))
14		meaiuninclem.b	. . . . . . . 8 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
15	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
16		simp1 1137	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝜑 ∧ 𝑛 ∈ 𝑍))
17		simp2 1138	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ)
18		simp3 1139	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
19	16	simprd 495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑛 ∈ 𝑍)
20		rspa 3248	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
21	18, 19, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
22	12	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
23		rexr 11307	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
24	23	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ^*)
25	5	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈ ℝ^*)
26		simp3 1139	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
27		ltpnf 13162	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
28	27	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞)
29	22, 24, 25, 26, 28	xrlelttrd 13202	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
30	16, 17, 21, 29	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
31	30	3exp 1120	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)))
32	31	rexlimdv 3153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))
33	15, 32	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞)
34	4, 6, 12, 13, 33	elicod 13437	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞))
35		meaiuninclem.s	. . . . 5 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
36	34, 35	fmptd 7134	. . . 4 ⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞))
37		rge0ssre 13496	. . . . 5 ⊢ (0[,)+∞) ⊆ ℝ
38	37	a1i 11	. . . 4 ⊢ (𝜑 → (0[,)+∞) ⊆ ℝ)
39	36, 38	fssd 6753	. . 3 ⊢ (𝜑 → 𝑆:𝑍⟶ℝ)
40	1	peano2uzs 12944	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
41	40	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
42	10	ffvelcdmda 7104	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
43	41, 42	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
44		meaiuninclem.i	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))
45	8, 9, 11, 43, 44	meassle 46478	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))
46	35	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
47		fvexd 6921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V)
48	46, 47	fvmpt2d 7029	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛)))
49		2fveq3 6911	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚)))
50	49	cbvmptv 5255	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
51	35, 50	eqtri 2765	. . . . . 6 ⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
52		2fveq3 6911	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1))))
53		fvexd 6921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V)
54	51, 52, 41, 53	fvmptd3 7039	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1))))
55	48, 54	breq12d 5156	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))))
56	45, 55	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)))
57	48	eqcomd 2743	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛))
58	57	breq1d 5153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥))
59	58	ralbidva 3176	. . . . . . 7 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
60	59	biimpd 229	. . . . . 6 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
61	60	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
62	61	reximdva 3168	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
63	14, 62	mpd 15	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)
64	1, 2, 39, 56, 63	climsup 15706	. 2 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
65		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑛𝜑
66		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥𝜑
67		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
68		fvex 6919	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑛) ∈ V
69	68	difexi 5330	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V)
71		meaiuninclem.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
72	71	fvmpt2 7027	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
73	67, 70, 72	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
74	73	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
75	7, 9	dmmeasal 46467	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
76	75	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
77		fzoct 45395	. . . . . . . . . . . 12 ⊢ (𝑁..^𝑛) ≼ ω
78	77	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω)
79	10	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀)
80		fzossuz 45392	. . . . . . . . . . . . . . . 16 ⊢ (𝑁..^𝑛) ⊆ (ℤ_≥‘𝑁)
81	1	eqcomi 2746	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑁) = 𝑍
82	80, 81	sseqtri 4032	. . . . . . . . . . . . . . 15 ⊢ (𝑁..^𝑛) ⊆ 𝑍
83	82	sseli 3979	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍)
84	83	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍)
85	79, 84	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
86	85	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
87	76, 78, 86	saliuncl 46338	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀)
88		saldifcl2 46343	. . . . . . . . . 10 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
89	76, 11, 87, 88	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
90	74, 89	eqeltrd 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀)
91	8, 9, 90	meaxrcl 46476	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ ℝ^*)
92	8, 90	meage0 46490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛)))
93		difssd 4137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛))
94	74, 93	eqsstrd 4018	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛))
95	8, 9, 90, 11, 94	meassle 46478	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛)))
96	91, 12, 6, 95, 33	xrlelttrd 13202	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞)
97	4, 6, 91, 92, 96	elicod 13437	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞))
98		2fveq3 6911	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖)))
99	98	breq1d 5153	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥))
100	99	cbvralvw 3237	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
101	100	biimpi 216	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
102	101	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
103		eleq1w 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍))
104	103	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍)))
105		oveq2 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖))
106	105	sumeq1d 15736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
107	98, 106	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))
108	104, 107	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))))
109		eleq1w 2824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍))
110	109	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍)))
111		oveq2 7439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛))
112	111	iuneq1d 5019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
113	111	iuneq1d 5019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
114	112, 113	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))
115	110, 114	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))))
116		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛))
117	116	cbviunv 5040	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛))
119	65, 1, 10, 71	iundjiun 46475	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
120	119	simplld 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
121	120	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
122		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍)
123		rspa 3248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
124	121, 122, 123	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
125		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖))
126	125	cbviunv 5040	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
128	118, 124, 127	3eqtrd 2781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
129	115, 128	chvarvv 1998	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
130	67, 1	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑁))
131	130	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑁))
132		fvoveq1 7454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1)))
133	125, 132	sseq12d 4017	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))
134	104, 133	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))))
135	134, 44	chvarvv 1998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
136	84, 135	syldan 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
137	136	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
138	131, 137	iunincfi 45099	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛))
139	129, 138	eqtr2d 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
140	139	fveq2d 6910	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)))
141		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍)
142		elfzuz 13560	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ_≥‘𝑁))
143	142, 81	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍)
145		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
146	145	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀))
147	104, 146	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)))
148	147, 90	chvarvv 1998	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)
149	144, 148	syldan 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
150	149	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
151		fzct 45390	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁...𝑛) ≼ ω
152	151	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω)
153	144	ssd 45085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍)
154	119	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))
155	145	cbvdisjv 5121	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
156	154, 155	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
157		disjss1 5116	. . . . . . . . . . . . . . . . . . . 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 46481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) = (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))))
161		fzfid 14014	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin)
162		2fveq3 6911	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖)))
163	162	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))
164	104, 163	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))))
165	164, 97	chvarvv 1998	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
166	144, 165	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
167	166	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
168	161, 167	sge0fsummpt 46405	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)))
169		2fveq3 6911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚)))
170	169	cbvsumv 15732	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))
171	170	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
172	168, 171	eqtrd 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
173	140, 160, 172	3eqtrd 2781	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
174	108, 173	chvarvv 1998	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
175		2fveq3 6911	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛)))
176	175	cbvsumv 15732	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))
177	176	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
178	174, 177	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
179	178	breq1d 5153	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
180	179	ralbidva 3176	. . . . . . . . . . . 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 3170	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
186	14, 185	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
187	65, 66, 2, 1, 97, 186	sge0reuzb 46463	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
188	98	cbvmptv 5255	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
189	35, 188	eqtri 2765	. . . . . . . . 9 ⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
190	189	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))))
191	178	mpteq2dva 5242	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
192	190, 191	eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
193	192	rneqd 5949	. . . . . 6 ⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
194	193	supeq1d 9486	. . . . 5 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
195	187, 194	eqtr4d 2780	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < ))
196	195	eqcomd 2743	. . 3 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
197	1	uzct 45068	. . . . . 6 ⊢ 𝑍 ≼ ω
198	197	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑍 ≼ ω)
199	65, 7, 9, 90, 198, 154	meadjiun 46481	. . . 4 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
200	199	eqcomd 2743	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
201	119	simplrd 770	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
202	201	fveq2d 6910	. . 3 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
203	196, 200, 202	3eqtrd 2781	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
204	64, 203	breqtrd 5169	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ∖ cdif 3948 ⊆ wss 3951 ∪ ciun 4991 Disj wdisj 5110 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ran crn 5686 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ωcom 7887 ≼ cdom 8983 supcsup 9480 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 +∞cpnf 11292 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 ℤcz 12613 ℤ_≥cuz 12878 [,)cico 13389 ...cfz 13547 ..^cfzo 13694 ⇝ cli 15520 Σcsu 15722 SAlgcsalg 46323 Σ^{^}csumge0 46377 Meascmea 46464

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-omul 8511 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-oi 9550 df-card 9979 df-acn 9982 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-z 12614 df-uz 12879 df-rp 13035 df-xadd 13155 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-clim 15524 df-sum 15723 df-salg 46324 df-sumge0 46378 df-mea 46465

This theorem is referenced by: meaiuninc 46496

W3C validator