Metamath Proof Explorer

Theorem meaiuninc3v

Description: Measures are continuous from below: if E is a sequence of nondecreasing measurable sets (with bounded measure) then the measure of the union is the limit of the measures. This is the general case of Proposition 112C (e) of Fremlin1 p. 16 . This theorem generalizes meaiuninc and meaiuninc2 where the sequence is required to be bounded. (Contributed by Glauco Siliprandi, 13-Feb-2022)

Ref Expression
Hypotheses meaiuninc3v.m ⊢ ( 𝜑 → 𝑀 ∈ Meas )
meaiuninc3v.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
meaiuninc3v.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
meaiuninc3v.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
meaiuninc3v.i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
meaiuninc3v.s ⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
Assertion meaiuninc3v ( 𝜑 → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 meaiuninc3v.m ⊢ ( 𝜑 → 𝑀 ∈ Meas )
2 meaiuninc3v.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3 meaiuninc3v.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
4 meaiuninc3v.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑀 )
5 meaiuninc3v.i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
6 meaiuninc3v.s ⊢ 𝑆 = ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
7 2 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑁 ∈ ℤ )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑀 ∈ Meas )
9 eqid ⊢ dom 𝑀 = dom 𝑀
10 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑀 )
11 8 9 10 meaxrcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
12 11 6 fmptd ⊢ ( 𝜑 → 𝑆 : 𝑍 ⟶ ℝ* )
13 12 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑆 : 𝑍 ⟶ ℝ* )
14 nfv ⊢ Ⅎ 𝑛 𝜑
15 nfcv ⊢ Ⅎ 𝑛 ℝ
16 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥
17 15 16 nfrex ⊢ Ⅎ 𝑛 ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥
18 14 17 nfan ⊢ Ⅎ 𝑛 ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
19 nfcv ⊢ Ⅎ 𝑛 𝐸
20 1 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑀 ∈ Meas )
21 4 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝐸 : 𝑍 ⟶ dom 𝑀 )
22 5 adantlr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) )
23 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
24 18 19 20 7 3 21 22 23 6 meaiunincf ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑆 ⇝ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
25 7 3 13 24 climxlim2 ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
26 simpr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
27 2fveq3 ⊢ ( 𝑗 = 𝑛 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
28 27 breq2d ⊢ ( 𝑗 = 𝑛 → ( 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
29 28 cbvrexvw ⊢ ( ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
30 29 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ ∃ 𝑛 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
31 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
32 31 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ) → 𝑥 ∈ ℝ* )
33 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
34 32 33 xrltnled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ↔ ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
35 34 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑛 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
36 30 35 bitrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
37 36 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
38 rexnal ⊢ ( ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ¬ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
39 38 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
40 ralnex ⊢ ( ∀ 𝑥 ∈ ℝ ¬ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
41 39 40 bitri ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 )
42 41 a1i ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑛 ∈ 𝑍 ¬ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
43 37 42 bitrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ↔ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) )
45 26 44 mpbird ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
46 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
47 45 46 syldan ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
48 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ )
49 48 31 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ∈ ℝ* )
50 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 )
51 3 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
52 51 ad4ant24 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
53 12 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑆 ‘ 𝑛 ) ∈ ℝ* )
54 50 52 53 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑛 ) ∈ ℝ* )
55 eleq1w ⊢ ( 𝑛 = 𝑗 → ( 𝑛 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
56 55 anbi2d ⊢ ( 𝑛 = 𝑗 → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
57 2fveq3 ⊢ ( 𝑛 = 𝑗 → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
58 57 eleq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* ↔ ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ∈ ℝ* ) )
59 56 58 imbi12d ⊢ ( 𝑛 = 𝑗 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ∈ ℝ* ) ) )
60 59 11 chvarvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ∈ ℝ* )
61 60 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ∈ ℝ* )
62 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
63 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑀 ∈ Meas )
64 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ∈ dom 𝑀 )
65 64 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ∈ dom 𝑀 )
66 simp1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝜑 )
67 51 3adant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
68 66 67 10 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑀 )
69 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) )
70 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → 𝜑 )
71 3 uzssd3 ⊢ ( 𝑗 ∈ 𝑍 → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
72 71 adantr ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → ( ℤ≥ ‘ 𝑗 ) ⊆ 𝑍 )
73 elfzouz ⊢ ( 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
74 73 adantl ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
75 72 74 sseldd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → 𝑘 ∈ 𝑍 )
76 75 adantll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → 𝑘 ∈ 𝑍 )
77 eleq1w ⊢ ( 𝑛 = 𝑘 → ( 𝑛 ∈ 𝑍 ↔ 𝑘 ∈ 𝑍 ) )
78 77 anbi2d ⊢ ( 𝑛 = 𝑘 → ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ) )
79 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑘 ) )
80 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝐸 ‘ ( 𝑛 + 1 ) ) = ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
81 79 80 sseq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) )
82 78 81 imbi12d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ( 𝐸 ‘ ( 𝑛 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) ) ) )
83 82 5 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
84 70 76 83 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
85 84 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑘 ∈ ( 𝑗 ..^ 𝑛 ) ) → ( 𝐸 ‘ 𝑘 ) ⊆ ( 𝐸 ‘ ( 𝑘 + 1 ) ) )
86 69 85 ssinc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ( 𝐸 ‘ 𝑛 ) )
87 63 9 65 68 86 meassle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
88 fvexd ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ V )
89 6 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ V ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
90 51 88 89 syl2anc ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
91 90 3adant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑛 ) = ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
92 87 91 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ ( 𝑆 ‘ 𝑛 ) )
93 92 ad5ant135 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ ( 𝑆 ‘ 𝑛 ) )
94 49 61 54 62 93 xrltletrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 < ( 𝑆 ‘ 𝑛 ) )
95 49 54 94 xrltled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) )
96 95 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) )
97 96 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) ) )
98 97 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) ) )
99 98 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) ) )
100 99 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) )
101 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) )
102 6 101 nfcxfr ⊢ Ⅎ 𝑛 𝑆
103 102 2 3 12 xlimpnf ⊢ ( 𝜑 → ( 𝑆 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ( 𝑆 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝑆 ‘ 𝑛 ) ) )
105 100 104 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → 𝑆 ~~>* +∞ )
106 nfv ⊢ Ⅎ 𝑥 𝜑
107 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) )
108 106 107 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
109 rspa ⊢ ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
110 109 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
111 nfv ⊢ Ⅎ 𝑗 𝜑
112 nfcv ⊢ Ⅎ 𝑗 ℝ
113 nfre1 ⊢ Ⅎ 𝑗 ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) )
114 112 113 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) )
115 111 114 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
116 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ ℝ
117 115 116 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑥 ∈ ℝ )
118 nfv ⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
119 31 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → 𝑥 ∈ ℝ* )
120 1 9 dmmeasal ⊢ ( 𝜑 → dom 𝑀 ∈ SAlg )
121 3 uzct ⊢ 𝑍 ≼ ω
122 121 a1i ⊢ ( 𝜑 → 𝑍 ≼ ω )
123 120 122 10 saliuncl ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑀 )
124 1 9 123 meaxrcl ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
125 124 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
126 60 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ∈ ℝ* )
127 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) )
128 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑀 ∈ Meas )
129 123 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑀 )
130 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑗 ) )
131 130 ssiun2s ⊢ ( 𝑗 ∈ 𝑍 → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
132 131 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
133 128 9 64 129 132 meassle ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
134 133 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
135 119 126 125 127 134 xrltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → 𝑥 < ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
136 119 125 135 xrltled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
137 136 exp31 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑗 ∈ 𝑍 → ( 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) )
138 137 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑗 ∈ 𝑍 → ( 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) )
139 117 118 138 rexlimd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) → 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) )
140 110 139 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
141 108 140 ralrimia ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ∀ 𝑥 ∈ ℝ 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
142 xrpnf ⊢ ( ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* → ( ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = +∞ ↔ ∀ 𝑥 ∈ ℝ 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) )
143 124 142 syl ⊢ ( 𝜑 → ( ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = +∞ ↔ ∀ 𝑥 ∈ ℝ 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) )
144 143 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ( ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = +∞ ↔ ∀ 𝑥 ∈ ℝ 𝑥 ≤ ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) )
145 141 144 mpbird ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = +∞ )
146 105 145 breqtrrd ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 𝑥 < ( 𝑀 ‘ ( 𝐸 ‘ 𝑗 ) ) ) → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
147 47 146 syldan ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑥 ∈ ℝ ∀ 𝑛 ∈ 𝑍 ( 𝑀 ‘ ( 𝐸 ‘ 𝑛 ) ) ≤ 𝑥 ) → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )
148 25 147 pm2.61dan ⊢ ( 𝜑 → 𝑆 ~~>* ( 𝑀 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) )