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 46471

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 11197	. . . . . . 7 ⊢ 0 ∈ ℝ^*
4	3	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ∈ ℝ^*)
5		pnfxr 11204	. . . . . . 7 ⊢ +∞ ∈ ℝ^*
6	5	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → +∞ ∈ ℝ^*)
7		meaiuninclem.m	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ Meas)
8	7	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
9		eqid 2729	. . . . . . 7 ⊢ dom 𝑀 = dom 𝑀
10		meaiuninclem.e	. . . . . . . 8 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
11	10	ffvelcdmda 7038	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
12	8, 9, 11	meaxrcl 46452	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
13	8, 11	meage0 46466	. . . . . 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 3224	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
21	18, 19, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
22	12	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ^*)
23		rexr 11196	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℝ^*)
24	23	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ^*)
25	5	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → +∞ ∈ ℝ^*)
26		simp3 1138	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) ≤ 𝑥)
27		ltpnf 13056	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 < +∞)
28	27	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → 𝑥 < +∞)
29	22, 24, 25, 26, 28	xrlelttrd 13096	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
30	16, 17, 21, 29	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → (𝑀‘(𝐸‘𝑛)) < +∞)
31	30	3exp 1119	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ ℝ → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞)))
32	31	rexlimdv 3132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → (𝑀‘(𝐸‘𝑛)) < +∞))
33	15, 32	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) < +∞)
34	4, 6, 12, 13, 33	elicod 13332	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ (0[,)+∞))
35		meaiuninclem.s	. . . . 5 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
36	34, 35	fmptd 7068	. . . 4 ⊢ (𝜑 → 𝑆:𝑍⟶(0[,)+∞))
37		rge0ssre 13393	. . . . 5 ⊢ (0[,)+∞) ⊆ ℝ
38	37	a1i 11	. . . 4 ⊢ (𝜑 → (0[,)+∞) ⊆ ℝ)
39	36, 38	fssd 6687	. . 3 ⊢ (𝜑 → 𝑆:𝑍⟶ℝ)
40	1	peano2uzs 12837	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
41	40	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
42	10	ffvelcdmda 7038	. . . . . 6 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
43	41, 42	syldan 591	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
44		meaiuninclem.i	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)))
45	8, 9, 11, 43, 44	meassle 46454	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))
46	35	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
47		fvexd 6855	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) ∈ V)
48	46, 47	fvmpt2d 6963	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = (𝑀‘(𝐸‘𝑛)))
49		2fveq3 6845	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑚)))
50	49	cbvmptv 5206	. . . . . . 7 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
51	35, 50	eqtri 2752	. . . . . 6 ⊢ 𝑆 = (𝑚 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑚)))
52		2fveq3 6845	. . . . . 6 ⊢ (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸‘𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1))))
53		fvexd 6855	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V)
54	51, 52, 41, 53	fvmptd3 6973	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1))))
55	48, 54	breq12d 5115	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸‘𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))))
56	45, 55	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) ≤ (𝑆‘(𝑛 + 1)))
57	48	eqcomd 2735	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑆‘𝑛))
58	57	breq1d 5112	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑆‘𝑛) ≤ 𝑥))
59	58	ralbidva 3154	. . . . . . 7 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
60	59	biimpd 229	. . . . . 6 ⊢ (𝜑 → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
61	60	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
62	61	reximdva 3146	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥))
63	14, 62	mpd 15	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑆‘𝑛) ≤ 𝑥)
64	1, 2, 39, 56, 63	climsup 15612	. 2 ⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
65		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑛𝜑
66		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑥𝜑
67		id 22	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍)
68		fvex 6853	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝑛) ∈ V
69	68	difexi 5280	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V
70	69	a1i 11	. . . . . . . . . . 11 ⊢ (𝑛 ∈ 𝑍 → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V)
71		meaiuninclem.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
72	71	fvmpt2 6961	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ 𝑍 ∧ ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ V) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
73	67, 70, 72	syl2anc 584	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
74	73	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)))
75	7, 9	dmmeasal 46443	. . . . . . . . . . 11 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
76	75	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
77		fzoct 45373	. . . . . . . . . . . 12 ⊢ (𝑁..^𝑛) ≼ ω
78	77	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁..^𝑛) ≼ ω)
79	10	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀)
80		fzossuz 45370	. . . . . . . . . . . . . . . 16 ⊢ (𝑁..^𝑛) ⊆ (ℤ_≥‘𝑁)
81	1	eqcomi 2738	. . . . . . . . . . . . . . . 16 ⊢ (ℤ_≥‘𝑁) = 𝑍
82	80, 81	sseqtri 3992	. . . . . . . . . . . . . . 15 ⊢ (𝑁..^𝑛) ⊆ 𝑍
83	82	sseli 3939	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑁..^𝑛) → 𝑖 ∈ 𝑍)
84	83	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → 𝑖 ∈ 𝑍)
85	79, 84	ffvelcdmd 7039	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
86	85	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ∈ dom 𝑀)
87	76, 78, 86	saliuncl 46314	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀)
88		saldifcl2 46319	. . . . . . . . . 10 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝑛) ∈ dom 𝑀 ∧ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖) ∈ dom 𝑀) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
89	76, 11, 87, 88	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ∈ dom 𝑀)
90	74, 89	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀)
91	8, 9, 90	meaxrcl 46452	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ ℝ^*)
92	8, 90	meage0 46466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 0 ≤ (𝑀‘(𝐹‘𝑛)))
93		difssd 4096	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝑛) ∖ ∪ 𝑖 ∈ (𝑁..^𝑛)(𝐸‘𝑖)) ⊆ (𝐸‘𝑛))
94	74, 93	eqsstrd 3978	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ⊆ (𝐸‘𝑛))
95	8, 9, 90, 11, 94	meassle 46454	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ≤ (𝑀‘(𝐸‘𝑛)))
96	91, 12, 6, 95, 33	xrlelttrd 13096	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) < +∞)
97	4, 6, 91, 92, 96	elicod 13332	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞))
98		2fveq3 6845	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐸‘𝑛)) = (𝑀‘(𝐸‘𝑖)))
99	98	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸‘𝑖)) ≤ 𝑥))
100	99	cbvralvw 3213	. . . . . . . . . . . 12 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 ↔ ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
101	100	biimpi 216	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
102	101	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥) → ∀𝑖 ∈ 𝑍 (𝑀‘(𝐸‘𝑖)) ≤ 𝑥)
103		eleq1w 2811	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → (𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍))
104	103	anbi2d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑖 ∈ 𝑍)))
105		oveq2 7377	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖))
106	105	sumeq1d 15642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
107	98, 106	eqeq12d 2745	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)) ↔ (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚))))
108	104, 107	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))))
109		eleq1w 2811	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → (𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍))
110	109	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → ((𝜑 ∧ 𝑚 ∈ 𝑍) ↔ (𝜑 ∧ 𝑛 ∈ 𝑍)))
111		oveq2 7377	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛))
112	111	iuneq1d 4979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
113	111	iuneq1d 4979	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑚 = 𝑛 → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
114	112, 113	eqeq12d 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑚 = 𝑛 → (∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖) ↔ ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖)))
115	110, 114	imbi12d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑚 = 𝑛 → (((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)) ↔ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))))
116		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 = 𝑛 → (𝐹‘𝑖) = (𝐹‘𝑛))
117	116	cbviunv 4999	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛)
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛))
119	65, 1, 10, 71	iundjiun 46451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
120	119	simplld 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
121	120	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
122		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍)
123		rspa 3224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
124	121, 122, 123	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛))
125		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐸‘𝑛) = (𝐸‘𝑖))
126	125	cbviunv 4999	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖)
127	126	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑛 ∈ (𝑁...𝑚)(𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
128	118, 124, 127	3eqtrd 2768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑚)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑚)(𝐸‘𝑖))
129	115, 128	chvarvv 1989	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖))
130	67, 1	eleqtrdi 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ_≥‘𝑁))
131	130	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ (ℤ_≥‘𝑁))
132		fvoveq1 7392	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1)))
133	125, 132	sseq12d 3977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → ((𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1))))
134	104, 133	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))))
135	134, 44	chvarvv 1989	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
136	84, 135	syldan 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
137	136	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸‘𝑖) ⊆ (𝐸‘(𝑖 + 1)))
138	131, 137	iunincfi 45081	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∪ 𝑖 ∈ (𝑁...𝑛)(𝐸‘𝑖) = (𝐸‘𝑛))
139	129, 138	eqtr2d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) = ∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖))
140	139	fveq2d 6844	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)))
141		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑛 ∈ 𝑍)
142		elfzuz 13457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ_≥‘𝑁))
143	142, 81	eleqtrdi 2838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ 𝑍)
144	143	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → 𝑖 ∈ 𝑍)
145		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → (𝐹‘𝑛) = (𝐹‘𝑖))
146	145	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → ((𝐹‘𝑛) ∈ dom 𝑀 ↔ (𝐹‘𝑖) ∈ dom 𝑀))
147	104, 146	imbi12d 344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ dom 𝑀) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)))
148	147, 90	chvarvv 1989	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐹‘𝑖) ∈ dom 𝑀)
149	144, 148	syldan 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
150	149	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹‘𝑖) ∈ dom 𝑀)
151		fzct 45368	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁...𝑛) ≼ ω
152	151	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ≼ ω)
153	144	ssd 45067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑁...𝑛) ⊆ 𝑍)
154	119	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))
155	145	cbvdisjv 5080	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛) ↔ Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
156	154, 155	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → Disj 𝑖 ∈ 𝑍 (𝐹‘𝑖))
157		disjss1 5075	. . . . . . . . . . . . . . . . . . . 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 46457	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘∪ 𝑖 ∈ (𝑁...𝑛)(𝐹‘𝑖)) = (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))))
161		fzfid 13914	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁...𝑛) ∈ Fin)
162		2fveq3 6845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑖 → (𝑀‘(𝐹‘𝑛)) = (𝑀‘(𝐹‘𝑖)))
163	162	eleq1d 2813	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑖 → ((𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞)))
164	104, 163	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑖 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐹‘𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))))
165	164, 97	chvarvv 1989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
166	144, 165	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
167	166	adantlr 715	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹‘𝑖)) ∈ (0[,)+∞))
168	161, 167	sge0fsummpt 46381	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)))
169		2fveq3 6845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑚 → (𝑀‘(𝐹‘𝑖)) = (𝑀‘(𝐹‘𝑚)))
170	169	cbvsumv 15638	. . . . . . . . . . . . . . . . . . 19 ⊢ Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚))
171	170	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
172	168, 171	eqtrd 2764	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (Σ^{^}‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹‘𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
173	140, 160, 172	3eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐸‘𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹‘𝑚)))
174	108, 173	chvarvv 1989	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)))
175		2fveq3 6845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → (𝑀‘(𝐹‘𝑚)) = (𝑀‘(𝐹‘𝑛)))
176	175	cbvsumv 15638	. . . . . . . . . . . . . . . 16 ⊢ Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))
177	176	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
178	174, 177	eqtrd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝑀‘(𝐸‘𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)))
179	178	breq1d 5112	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ((𝑀‘(𝐸‘𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
180	179	ralbidva 3154	. . . . . . . . . . . 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 3148	. . . . . . 7 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛 ∈ 𝑍 (𝑀‘(𝐸‘𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥))
186	14, 185	mpd 15	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖 ∈ 𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛)) ≤ 𝑥)
187	65, 66, 2, 1, 97, 186	sge0reuzb 46439	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
188	98	cbvmptv 5206	. . . . . . . . . 10 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
189	35, 188	eqtri 2752	. . . . . . . . 9 ⊢ 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖)))
190	189	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))))
191	178	mpteq2dva 5195	. . . . . . . 8 ⊢ (𝜑 → (𝑖 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑖))) = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
192	190, 191	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → 𝑆 = (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
193	192	rneqd 5891	. . . . . 6 ⊢ (𝜑 → ran 𝑆 = ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))))
194	193	supeq1d 9373	. . . . 5 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖 ∈ 𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹‘𝑛))), ℝ, < ))
195	187, 194	eqtr4d 2767	. . . 4 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = sup(ran 𝑆, ℝ, < ))
196	195	eqcomd 2735	. . 3 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
197	1	uzct 45050	. . . . . 6 ⊢ 𝑍 ≼ ω
198	197	a1i 11	. . . . 5 ⊢ (𝜑 → 𝑍 ≼ ω)
199	65, 7, 9, 90, 198, 154	meadjiun 46457	. . . 4 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))))
200	199	eqcomd 2735	. . 3 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐹‘𝑛)))) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)))
201	119	simplrd 769	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
202	201	fveq2d 6844	. . 3 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
203	196, 200, 202	3eqtrd 2768	. 2 ⊢ (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
204	64, 203	breqtrd 5128	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3444 ∖ cdif 3908 ⊆ wss 3911 ∪ ciun 4951 Disj wdisj 5069 class class class wbr 5102 ↦ cmpt 5183 dom cdm 5631 ran crn 5632 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 ωcom 7822 ≼ cdom 8893 supcsup 9367 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 +∞cpnf 11181 ℝ^*cxr 11183 < clt 11184 ≤ cle 11185 ℤcz 12505 ℤ_≥cuz 12769 [,)cico 13284 ...cfz 13444 ..^cfzo 13591 ⇝ cli 15426 Σcsu 15628 SAlgcsalg 46299 Σ^{^}csumge0 46353 Meascmea 46440

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 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

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 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-disj 5070 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-oadd 8415 df-omul 8416 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-oi 9439 df-card 9868 df-acn 9871 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-rp 12928 df-xadd 13049 df-ico 13288 df-icc 13289 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629 df-salg 46300 df-sumge0 46354 df-mea 46441

This theorem is referenced by: meaiuninc 46472

W3C validator