Metamath Proof Explorer

Theorem meaiuninclem

Description: Measures are continuous from below (bounded case): if E 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)

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

Proof

Step Hyp Ref Expression
1 meaiuninclem.m ⊢ ( 𝜑 → 𝑀 ∈ Meas )
2 meaiuninclem.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3 meaiuninclem.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
4 meaiuninclem.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
5 meaiuninclem.i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
6 meaiuninclem.b ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
7 meaiuninclem.s ⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
8 meaiuninclem.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
9 0xr ⊢ 0 ∈ ℝ*
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 0 ∈ ℝ* )
11 pnfxr ⊢ +∞ ∈ ℝ*
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → +∞ ∈ ℝ* )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑀 ∈ Meas )
14 eqid ⊢ dom 𝑀 = dom 𝑀
15 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑀 )
16 13 14 15 meaxrcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
17 13 15 meage0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 0 ≤ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
18 6 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
19 simp1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) )
20 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑥 ∈ ℝ )
21 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
22 19 simprd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑛 ∈ 𝑍 )
23 rspa ⊢ ( ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
24 21 22 23 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
25 16 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
26 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
27 26 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
28 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → +∞ ∈ ℝ* )
29 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
30 ltpnf ⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
31 30 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑥 < +∞ )
32 25 27 28 29 31 xrlelttrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ )
33 19 20 24 32 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ )
34 33 3exp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ ℝ → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ ) ) )
35 34 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ ) )
36 18 35 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) < +∞ )
37 10 12 16 17 36 elicod ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) )
38 37 7 fmptd ⊢ ( 𝜑 → 𝑆 : 𝑍 ⟶ ( 0 [,) +∞ ) )
39 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
40 39 a1i ⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ℝ )
41 38 40 fssd ⊢ ( 𝜑 → 𝑆 : 𝑍 ⟶ ℝ )
42 3 peano2uzs ⊢ ( 𝑛 ∈ 𝑍 → ( 𝑛 + 1 ) ∈ 𝑍 )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑛 + 1 ) ∈ 𝑍 )
44 4 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ∈ dom 𝑀 )
45 43 44 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ ( 𝑛 + 1 ) ) ∈ dom 𝑀 )
46 13 14 15 45 5 meassle ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) )
47 7 a1i ⊢ ( 𝜑 → 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
48 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ V )
49 47 48 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
50 2fveq3 ⊢ ( 𝑛 = 𝑚 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) )
51 50 cbvmptv ⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) )
52 7 51 eqtri ⊢ 𝑆 = ( 𝑚 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) )
53 2fveq3 ⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) )
54 fvexd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) ∈ V )
55 52 53 43 54 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑆 ‘ ( 𝑛 + 1 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) )
56 49 55 breq12d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑆 ‘ 𝑛 ) ≤ ( 𝑆 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) ) )
57 46 56 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑛 ) ≤ ( 𝑆 ‘ ( 𝑛 + 1 ) ) )
58 49 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑆 ‘ 𝑛 ) )
59 58 breq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ( 𝑆 ‘ 𝑛 ) ≤ 𝑥 ) )
60 59 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ 𝑍 ( 𝑆 ‘ 𝑛 ) ≤ 𝑥 ) )
61 60 biimpd ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ∀ 𝑛 ∈ 𝑍 ( 𝑆 ‘ 𝑛 ) ≤ 𝑥 ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ∀ 𝑛 ∈ 𝑍 ( 𝑆 ‘ 𝑛 ) ≤ 𝑥 ) )
63 62 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑆 ‘ 𝑛 ) ≤ 𝑥 ) )
64 6 63 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑆 ‘ 𝑛 ) ≤ 𝑥 )
65 3 2 41 57 64 climsup ⊢ ( 𝜑 → 𝑆 ⇝ sup ( ran 𝑆 , ℝ , < ) )
66 nfv ⊢ Ⅎ 𝑛 𝜑
67 nfv ⊢ Ⅎ 𝑥 𝜑
68 id ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ 𝑍 )
69 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
70 69 difexi ⊢ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V
71 70 a1i ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V )
72 8 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
73 68 71 72 syl2anc ⊢ ( 𝑛 ∈ 𝑍 → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
75 1 14 dmmeasal ⊢ ( 𝜑 → dom 𝑀 ∈ SAlg )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → dom 𝑀 ∈ SAlg )
77 fzoct ⊢ ( 𝑁 ..^ 𝑛 ) ≼ ω
78 77 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑁 ..^ 𝑛 ) ≼ ω )
79 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝐸 : 𝑍 ⟶ dom 𝑀 )
80 fzossuz ⊢ ( 𝑁 ..^ 𝑛 ) ⊆ ( ℤ≥ ‘ 𝑁 )
81 3 eqcomi ⊢ ( ℤ≥ ‘ 𝑁 ) = 𝑍
82 80 81 sseqtri ⊢ ( 𝑁 ..^ 𝑛 ) ⊆ 𝑍
83 82 sseli ⊢ ( 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) → 𝑖 ∈ 𝑍 )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → 𝑖 ∈ 𝑍 )
85 79 84 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝐸 ‘ 𝑖 ) ∈ dom 𝑀 )
86 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝐸 ‘ 𝑖 ) ∈ dom 𝑀 )
87 76 78 86 saliuncl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ∈ dom 𝑀 )
88 saldifcl2 ⊢ ( ( dom 𝑀 ∈ SAlg ∧ ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑀 ∧ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ∈ dom 𝑀 ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ dom 𝑀 )
89 76 15 87 88 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ∈ dom 𝑀 )
90 74 89 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ dom 𝑀 )
91 13 14 90 meaxrcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ* )
92 13 90 meage0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 0 ≤ ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) )
93 difssd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ⊆ ( 𝐸 ‘ 𝑛 ) )
94 74 93 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ 𝑛 ) )
95 13 14 90 15 94 meassle ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
96 91 16 12 95 36 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) < +∞ )
97 10 12 91 92 96 elicod ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) )
98 2fveq3 ⊢ ( 𝑛 = 𝑖 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) )
99 98 breq1d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 ) )
100 99 cbvralvw ⊢ ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑖 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 )
101 100 biimpi ⊢ ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ∀ 𝑖 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 )
102 101 adantl ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ∀ 𝑖 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 )
103 eleq1w ⊢ ( 𝑛 = 𝑖 → ( 𝑛 ∈ 𝑍 ↔ 𝑖 ∈ 𝑍 ) )
104 103 anbi2d ⊢ ( 𝑛 = 𝑖 → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ) )
105 oveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝑁 ... 𝑛 ) = ( 𝑁 ... 𝑖 ) )
106 105 sumeq1d ⊢ ( 𝑛 = 𝑖 → Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) )
107 98 106 eqeq12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) ↔ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
108 104 107 imbi12d ⊢ ( 𝑛 = 𝑖 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) ) ) )
109 eleq1w ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ 𝑍 ↔ 𝑛 ∈ 𝑍 ) )
110 109 anbi2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ) )
111 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝑁 ... 𝑚 ) = ( 𝑁 ... 𝑛 ) )
112 111 iuneq1d ⊢ ( 𝑚 = 𝑛 → ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) )
113 111 iuneq1d ⊢ ( 𝑚 = 𝑛 → ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
114 112 113 eqeq12d ⊢ ( 𝑚 = 𝑛 → ( ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑖 ) ↔ ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
115 110 114 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑖 ) ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) ) )
116 fveq2 ⊢ ( 𝑖 = 𝑛 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑛 ) )
117 116 cbviunv ⊢ ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 )
118 117 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) )
119 66 3 4 8 iundjiun ⊢ ( 𝜑 → ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ∧ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∧ Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) )
120 119 simplld ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
122 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
123 rspa ⊢ ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
124 121 122 123 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) )
125 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑖 ) )
126 125 cbviunv ⊢ ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑖 )
127 126 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑛 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑖 ) )
128 118 124 127 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑚 ) ( 𝐸 ‘ 𝑖 ) )
129 115 128 chvarvv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
130 68 3 eleqtrdi ⊢ ( 𝑛 ∈ 𝑍 → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
131 130 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) )
132 fvoveq1 ⊢ ( 𝑛 = 𝑖 → ( 𝐸 ‘ ( 𝑛 + 1 ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
133 125 132 sseq12d ⊢ ( 𝑛 = 𝑖 → ( ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐸 ‘ 𝑖 ) ⊆ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
134 104 133 imbi12d ⊢ ( 𝑛 = 𝑖 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑖 ) ⊆ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
135 134 5 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑖 ) ⊆ ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
136 84 135 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝐸 ‘ 𝑖 ) ⊆ ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
137 136 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑖 ∈ ( 𝑁 ..^ 𝑛 ) ) → ( 𝐸 ‘ 𝑖 ) ⊆ ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
138 131 137 iunincfi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑛 ) )
139 129 138 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) = ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) )
140 139 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) ) )
141 nfv ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑛 ∈ 𝑍 )
142 elfzuz ⊢ ( 𝑖 ∈ ( 𝑁 ... 𝑛 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑁 ) )
143 142 81 eleqtrdi ⊢ ( 𝑖 ∈ ( 𝑁 ... 𝑛 ) → 𝑖 ∈ 𝑍 )
144 143 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ) → 𝑖 ∈ 𝑍 )
145 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑖 ) )
146 145 eleq1d ⊢ ( 𝑛 = 𝑖 → ( ( 𝐹 ‘ 𝑛 ) ∈ dom 𝑀 ↔ ( 𝐹 ‘ 𝑖 ) ∈ dom 𝑀 ) )
147 104 146 imbi12d ⊢ ( 𝑛 = 𝑖 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ dom 𝑀 ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝑀 ) ) )
148 147 90 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝑀 )
149 144 148 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝑀 )
150 149 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom 𝑀 )
151 fzct ⊢ ( 𝑁 ... 𝑛 ) ≼ ω
152 151 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑁 ... 𝑛 ) ≼ ω )
153 144 ssd ⊢ ( 𝜑 → ( 𝑁 ... 𝑛 ) ⊆ 𝑍 )
154 119 simprd ⊢ ( 𝜑 → Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) )
155 145 cbvdisjv ⊢ ( Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ↔ Disj 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) )
156 154 155 sylib ⊢ ( 𝜑 → Disj 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) )
157 disjss1 ⊢ ( ( 𝑁 ... 𝑛 ) ⊆ 𝑍 → ( Disj 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) → Disj 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) ) )
158 153 156 157 sylc ⊢ ( 𝜑 → Disj 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) )
159 158 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Disj 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) )
160 141 13 14 150 152 159 meadjiun ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ∪ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝐹 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑖 ∈ ( 𝑁 ... 𝑛 ) ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) )
161 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑁 ... 𝑛 ) ∈ Fin )
162 2fveq3 ⊢ ( 𝑛 = 𝑖 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) )
163 162 eleq1d ⊢ ( 𝑛 = 𝑖 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( 0 [,) +∞ ) ) )
164 104 163 imbi12d ⊢ ( 𝑛 = 𝑖 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( 0 [,) +∞ ) ) ) )
165 164 97 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( 0 [,) +∞ ) )
166 144 165 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( 0 [,) +∞ ) )
167 166 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( 0 [,) +∞ ) )
168 161 167 sge0fsummpt ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( Σ^ ‘ ( 𝑖 ∈ ( 𝑁 ... 𝑛 ) ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) = Σ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) )
169 2fveq3 ⊢ ( 𝑖 = 𝑚 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) )
170 169 cbvsumv ⊢ Σ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) )
171 170 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → Σ 𝑖 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) )
172 168 171 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( Σ^ ‘ ( 𝑖 ∈ ( 𝑁 ... 𝑛 ) ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) )
173 140 160 172 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑛 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) )
174 108 173 chvarvv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) = Σ 𝑚 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) )
175 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) = ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) )
176 175 cbvsumv ⊢ Σ 𝑚 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) )
177 176 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → Σ 𝑚 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) )
178 174 177 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) = Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) )
179 178 breq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 ↔ Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ) )
180 179 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 ↔ ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ) )
181 180 biimpd ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 → ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ) )
182 181 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑖 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ≤ 𝑥 ) → ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 )
183 102 182 syldan ⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 )
184 183 ex ⊢ ( 𝜑 → ( ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ) )
185 184 reximdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 ) )
186 6 185 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ≤ 𝑥 )
187 66 67 2 3 97 186 sge0reuzb ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = sup ( ran ( 𝑖 ∈ 𝑍 ↦ Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ , < ) )
188 98 cbvmptv ⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑖 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) )
189 7 188 eqtri ⊢ 𝑆 = ( 𝑖 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) )
190 189 a1i ⊢ ( 𝜑 → 𝑆 = ( 𝑖 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ) )
191 178 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑖 ) ) ) = ( 𝑖 ∈ 𝑍 ↦ Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
192 190 191 eqtrd ⊢ ( 𝜑 → 𝑆 = ( 𝑖 ∈ 𝑍 ↦ Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
193 192 rneqd ⊢ ( 𝜑 → ran 𝑆 = ran ( 𝑖 ∈ 𝑍 ↦ Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
194 193 supeq1d ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ , < ) = sup ( ran ( 𝑖 ∈ 𝑍 ↦ Σ 𝑛 ∈ ( 𝑁 ... 𝑖 ) ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) , ℝ , < ) )
195 187 194 eqtr4d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = sup ( ran 𝑆 , ℝ , < ) )
196 195 eqcomd ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ , < ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
197 3 uzct ⊢ 𝑍 ≼ ω
198 197 a1i ⊢ ( 𝜑 → 𝑍 ≼ ω )
199 66 1 14 90 198 154 meadjiun ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) )
200 199 eqcomd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ) = ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) )
201 119 simplrd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
202 201 fveq2d ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) = ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
203 196 200 202 3eqtrd ⊢ ( 𝜑 → sup ( ran 𝑆 , ℝ , < ) = ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
204 65 203 breqtrd ⊢ ( 𝜑 → 𝑆 ⇝ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )