Metamath Proof Explorer

Theorem caratheodorylem1

Description: Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of Fremlin1 p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caratheodorylem1.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
caratheodorylem1.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
caratheodorylem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
caratheodorylem1.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
caratheodorylem1.dj ⊢ ( 𝜑 → Disj 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
caratheodorylem1.g ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
caratheodorylem1.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
Assertion caratheodorylem1 ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 caratheodorylem1.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 caratheodorylem1.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 caratheodorylem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 caratheodorylem1.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
5 caratheodorylem1.dj ⊢ ( 𝜑 → Disj 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
6 caratheodorylem1.g ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
7 caratheodorylem1.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
9 7 8 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
10 id ⊢ ( 𝜑 → 𝜑 )
11 2fveq3 ⊢ ( 𝑗 = 𝑀 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) )
12 oveq2 ⊢ ( 𝑗 = 𝑀 → ( 𝑀 ... 𝑗 ) = ( 𝑀 ... 𝑀 ) )
13 12 mpteq1d ⊢ ( 𝑗 = 𝑀 → ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
14 13 fveq2d ⊢ ( 𝑗 = 𝑀 → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
15 11 14 eqeq12d ⊢ ( 𝑗 = 𝑀 → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ↔ ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
16 15 imbi2d ⊢ ( 𝑗 = 𝑀 → ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ) )
17 2fveq3 ⊢ ( 𝑗 = 𝑖 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) )
18 oveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑀 ... 𝑗 ) = ( 𝑀 ... 𝑖 ) )
19 18 mpteq1d ⊢ ( 𝑗 = 𝑖 → ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
20 19 fveq2d ⊢ ( 𝑗 = 𝑖 → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
21 17 20 eqeq12d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ↔ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
22 21 imbi2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ) )
23 2fveq3 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) )
24 oveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑀 ... 𝑗 ) = ( 𝑀 ... ( 𝑖 + 1 ) ) )
25 24 mpteq1d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
26 25 fveq2d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
27 23 26 eqeq12d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ↔ ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
28 27 imbi2d ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ) )
29 2fveq3 ⊢ ( 𝑗 = 𝑁 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) )
30 oveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝑀 ... 𝑗 ) = ( 𝑀 ... 𝑁 ) )
31 30 mpteq1d ⊢ ( 𝑗 = 𝑁 → ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
32 31 fveq2d ⊢ ( 𝑗 = 𝑁 → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
33 29 32 eqeq12d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ↔ ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
34 33 imbi2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑗 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑗 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ↔ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ) )
35 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
36 7 35 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
37 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
38 36 37 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
39 38 mpteq1d ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
40 39 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
41 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → 𝑂 ∈ OutMeas )
42 eqid ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
43 2 caragenss ⊢ ( 𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂 )
44 41 43 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → 𝑆 ⊆ dom 𝑂 )
45 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → 𝐸 : 𝑍 ⟶ 𝑆 )
46 elsni ⊢ ( 𝑛 ∈ { 𝑀 } → 𝑛 = 𝑀 )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → 𝑛 = 𝑀 )
48 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
49 36 48 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
50 49 3 eleqtrrdi ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → 𝑀 ∈ 𝑍 )
52 47 51 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → 𝑛 ∈ 𝑍 )
53 45 52 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 )
54 44 53 sseldd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑂 )
55 elssuni ⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑂 → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
56 54 55 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
57 41 42 56 omecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
58 eqid ⊢ ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
59 57 58 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : { 𝑀 } ⟶ ( 0 [,] +∞ ) )
60 36 59 sge0sn ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑀 ) )
61 eqidd ⊢ ( 𝜑 → ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
62 38 iuneq1d ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ { 𝑀 } ( 𝐸 ‘ 𝑖 ) )
63 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑀 ) )
64 63 iunxsng ⊢ ( 𝑀 ∈ 𝑍 → ∪ 𝑖 ∈ { 𝑀 } ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑀 ) )
65 50 64 syl ⊢ ( 𝜑 → ∪ 𝑖 ∈ { 𝑀 } ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑀 ) )
66 eqidd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑀 ) = ( 𝐸 ‘ 𝑀 ) )
67 62 65 66 3eqtrrd ⊢ ( 𝜑 → ( 𝐸 ‘ 𝑀 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( 𝐸 ‘ 𝑀 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
69 fveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑀 ) )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑀 ) )
71 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑀 ) )
72 71 iuneq1d ⊢ ( 𝑛 = 𝑀 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
73 ovex ⊢ ( 𝑀 ... 𝑀 ) ∈ V
74 fvex ⊢ ( 𝐸 ‘ 𝑖 ) ∈ V
75 73 74 iunex ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) ∈ V
76 75 a1i ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) ∈ V )
77 6 72 50 76 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( 𝐺 ‘ 𝑀 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
79 68 70 78 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( 𝐸 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑀 ) )
80 79 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 = 𝑀 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) )
81 snidg ⊢ ( 𝑀 ∈ 𝑍 → 𝑀 ∈ { 𝑀 } )
82 50 81 syl ⊢ ( 𝜑 → 𝑀 ∈ { 𝑀 } )
83 fvexd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) ∈ V )
84 61 80 82 83 fvmptd ⊢ ( 𝜑 → ( ( 𝑛 ∈ { 𝑀 } ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ‘ 𝑀 ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) )
85 40 60 84 3eqtrrd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
86 85 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑀 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑀 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
87 simp3 ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ∧ 𝜑 ) → 𝜑 )
88 simp1 ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ∧ 𝜑 ) → 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) )
89 id ⊢ ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
90 89 imp ⊢ ( ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ∧ 𝜑 ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
91 90 3adant1 ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ∧ 𝜑 ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
92 elfzoel1 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℤ )
93 elfzoelz ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 ∈ ℤ )
94 93 peano2zd ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ℤ )
95 92 94 94 3jca ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ) )
96 92 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℝ )
97 94 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ℝ )
98 93 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 ∈ ℝ )
99 elfzole1 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑖 )
100 98 ltp1d ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 < ( 𝑖 + 1 ) )
101 96 98 97 99 100 lelttrd ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 < ( 𝑖 + 1 ) )
102 96 97 101 ltled ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ ( 𝑖 + 1 ) )
103 leid ⊢ ( ( 𝑖 + 1 ) ∈ ℝ → ( 𝑖 + 1 ) ≤ ( 𝑖 + 1 ) )
104 97 103 syl ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ≤ ( 𝑖 + 1 ) )
105 95 102 104 jca32 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ) ∧ ( 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ ( 𝑖 + 1 ) ) ) )
106 elfz2 ⊢ ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↔ ( ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ) ∧ ( 𝑀 ≤ ( 𝑖 + 1 ) ∧ ( 𝑖 + 1 ) ≤ ( 𝑖 + 1 ) ) ) )
107 105 106 sylibr ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) )
108 107 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) )
109 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝐸 ‘ 𝑗 ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
110 109 ssiun2s ⊢ ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
111 108 110 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
112 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑗 ) )
113 112 cbviunv ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 )
114 113 mpteq2i ⊢ ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) )
115 6 114 eqtri ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) )
116 oveq2 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... ( 𝑖 + 1 ) ) )
117 116 iuneq1d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
118 36 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℤ )
119 93 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ ℤ )
120 119 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ℤ )
121 118 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
122 120 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
123 119 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ ℝ )
124 99 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ 𝑖 )
125 123 ltp1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 < ( 𝑖 + 1 ) )
126 121 123 122 124 125 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 < ( 𝑖 + 1 ) )
127 121 122 126 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
128 118 120 127 3jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ) )
129 eluz2 ⊢ ( ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ) )
130 128 129 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
131 3 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
132 130 131 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ 𝑍 )
133 ovex ⊢ ( 𝑀 ... ( 𝑖 + 1 ) ) ∈ V
134 fvex ⊢ ( 𝐸 ‘ 𝑗 ) ∈ V
135 133 134 iunex ⊢ ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ∈ V
136 135 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ∈ V )
137 115 117 132 136 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑖 + 1 ) ) = ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
138 137 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑖 + 1 ) ) )
139 111 138 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐺 ‘ ( 𝑖 + 1 ) ) )
140 sseqin2 ⊢ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ↔ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
141 140 biimpi ⊢ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐺 ‘ ( 𝑖 + 1 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
142 139 141 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
143 142 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
144 nfcv ⊢ Ⅎ 𝑗 ( 𝐸 ‘ ( 𝑖 + 1 ) )
145 elfzouz ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
146 145 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
147 144 146 109 iunp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) = ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
148 137 147 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑖 + 1 ) ) = ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
149 148 difeq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
150 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑗 ) )
151 150 cbvdisjv ⊢ ( Disj 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ↔ Disj 𝑗 ∈ 𝑍 ( 𝐸 ‘ 𝑗 ) )
152 5 151 sylib ⊢ ( 𝜑 → Disj 𝑗 ∈ 𝑍 ( 𝐸 ‘ 𝑗 ) )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → Disj 𝑗 ∈ 𝑍 ( 𝐸 ‘ 𝑗 ) )
154 fzssuz ⊢ ( 𝑀 ... 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 )
155 154 131 sseqtri ⊢ ( 𝑀 ... 𝑖 ) ⊆ 𝑍
156 155 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ... 𝑖 ) ⊆ 𝑍 )
157 fzp1nel ⊢ ¬ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑖 )
158 157 a1i ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ¬ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑖 ) )
159 158 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ¬ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑖 ) )
160 132 159 eldifd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 𝑍 ∖ ( 𝑀 ... 𝑖 ) ) )
161 153 156 160 109 disjiun2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅ )
162 undif4 ⊢ ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅ → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
163 161 162 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
164 163 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
165 simpl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝜑 )
166 146 131 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ 𝑍 )
167 115 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) ) )
168 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 = 𝑖 ) → 𝑛 = 𝑖 )
169 168 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 = 𝑖 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑖 ) )
170 169 iuneq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 = 𝑖 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) )
171 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
172 ovex ⊢ ( 𝑀 ... 𝑖 ) ∈ V
173 172 134 iunex ⊢ ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∈ V
174 173 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∈ V )
175 167 170 171 174 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑖 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) )
176 165 166 175 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝑖 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) )
177 176 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑖 ) )
178 difid ⊢ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅
179 178 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅ )
180 177 179 uneq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝐺 ‘ 𝑖 ) ∪ ∅ ) )
181 un0 ⊢ ( ( 𝐺 ‘ 𝑖 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑖 )
182 181 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝑖 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑖 ) )
183 180 182 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ‘ 𝑖 ) )
184 149 164 183 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐺 ‘ 𝑖 ) )
185 184 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) )
186 143 185 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
187 186 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
188 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑂 ∈ OutMeas )
189 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐸 : 𝑍 ⟶ 𝑆 )
190 189 132 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∈ 𝑆 )
191 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝜑 )
192 92 adantr ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑀 ∈ ℤ )
193 elfzelz ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑗 ∈ ℤ )
194 193 adantl ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ ℤ )
195 elfzle1 ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑀 ≤ 𝑗 )
196 195 adantl ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑀 ≤ 𝑗 )
197 192 194 196 3jca ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) )
198 eluz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) )
199 197 198 sylibr ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
200 199 131 eleqtrdi ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
201 200 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
202 1 43 syl ⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
203 202 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑆 ⊆ dom 𝑂 )
204 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝑆 )
205 203 204 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ∈ dom 𝑂 )
206 elssuni ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ dom 𝑂 → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
207 205 206 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
208 191 201 207 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
209 208 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
210 iunss ⊢ ( ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 ↔ ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
211 209 210 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
212 137 211 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ dom 𝑂 )
213 188 2 42 190 212 caragensplit ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) )
214 213 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) )
215 214 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) )
216 188 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑂 ∈ OutMeas )
217 165 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝜑 )
218 elfzuz ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
219 218 131 eleqtrdi ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑛 ∈ 𝑍 )
220 219 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑛 ∈ 𝑍 )
221 4 202 fssd ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑂 )
222 221 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑂 )
223 222 55 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
224 217 220 223 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
225 216 42 224 omecl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
226 2fveq3 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
227 146 225 226 sge0p1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
228 227 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
229 id ⊢ ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
230 229 eqcomd ⊢ ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) )
231 230 oveq1d ⊢ ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) → ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
232 231 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
233 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝜑 )
234 155 sseli ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) → 𝑗 ∈ 𝑍 )
235 234 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ∈ 𝑍 )
236 233 235 207 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
237 236 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
238 237 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
239 iunss ⊢ ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 ↔ ∀ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
240 238 239 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
241 175 240 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑖 ) ⊆ ∪ dom 𝑂 )
242 165 166 241 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝑖 ) ⊆ ∪ dom 𝑂 )
243 188 42 242 omexrcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ∈ ℝ* )
244 111 211 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ dom 𝑂 )
245 188 42 244 omexrcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∈ ℝ* )
246 243 245 xaddcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
247 246 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
248 228 232 247 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
249 187 215 248 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
250 87 88 91 249 syl3anc ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ∧ 𝜑 ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
251 250 3exp ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ) )
252 16 22 28 34 86 251 fzind2 ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
253 9 10 252 sylc ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )