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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ { 𝑀 } ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝑆 )
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 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ℝ )
96 94 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ℝ )
97 93 zred ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 ∈ ℝ )
98 elfzole1 ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ 𝑖 )
99 97 ltp1d ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 < ( 𝑖 + 1 ) )
100 95 97 96 98 99 lelttrd ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 < ( 𝑖 + 1 ) )
101 95 96 100 ltled ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ≤ ( 𝑖 + 1 ) )
102 leid ⊢ ( ( 𝑖 + 1 ) ∈ ℝ → ( 𝑖 + 1 ) ≤ ( 𝑖 + 1 ) )
103 96 102 syl ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ≤ ( 𝑖 + 1 ) )
104 92 94 94 101 103 elfzd ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) )
106 fveq2 ⊢ ( 𝑗 = ( 𝑖 + 1 ) → ( 𝐸 ‘ 𝑗 ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
107 106 ssiun2s ⊢ ( ( 𝑖 + 1 ) ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
108 105 107 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
109 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑗 ) )
110 109 cbviunv ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 )
111 110 mpteq2i ⊢ ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) )
112 6 111 eqtri ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) )
113 oveq2 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... ( 𝑖 + 1 ) ) )
114 113 iuneq1d ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
115 36 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℤ )
116 93 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ ℤ )
117 116 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ℤ )
118 115 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ∈ ℝ )
119 117 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
120 116 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ ℝ )
121 98 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ 𝑖 )
122 120 ltp1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 < ( 𝑖 + 1 ) )
123 118 120 119 121 122 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 < ( 𝑖 + 1 ) )
124 118 119 123 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑀 ≤ ( 𝑖 + 1 ) )
125 115 117 124 3jca ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ) )
126 eluz2 ⊢ ( ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑖 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑖 + 1 ) ) )
127 125 126 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
128 3 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
129 127 128 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ 𝑍 )
130 ovex ⊢ ( 𝑀 ... ( 𝑖 + 1 ) ) ∈ V
131 fvex ⊢ ( 𝐸 ‘ 𝑗 ) ∈ V
132 130 131 iunex ⊢ ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ∈ V
133 132 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ∈ V )
134 112 114 129 133 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑖 + 1 ) ) = ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) )
135 134 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) = ( 𝐺 ‘ ( 𝑖 + 1 ) ) )
136 108 135 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐺 ‘ ( 𝑖 + 1 ) ) )
137 sseqin2 ⊢ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ↔ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
138 137 biimpi ⊢ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ( 𝐺 ‘ ( 𝑖 + 1 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
139 136 138 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐸 ‘ ( 𝑖 + 1 ) ) )
140 139 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
141 nfcv ⊢ Ⅎ 𝑗 ( 𝐸 ‘ ( 𝑖 + 1 ) )
142 elfzouz ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
143 142 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
144 141 143 106 iunp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) = ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
145 134 144 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑖 + 1 ) ) = ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
146 145 difeq1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
147 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑗 ) )
148 147 cbvdisjv ⊢ ( Disj 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ↔ Disj 𝑗 ∈ 𝑍 ( 𝐸 ‘ 𝑗 ) )
149 5 148 sylib ⊢ ( 𝜑 → Disj 𝑗 ∈ 𝑍 ( 𝐸 ‘ 𝑗 ) )
150 149 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → Disj 𝑗 ∈ 𝑍 ( 𝐸 ‘ 𝑗 ) )
151 fzssuz ⊢ ( 𝑀 ... 𝑖 ) ⊆ ( ℤ≥ ‘ 𝑀 )
152 151 128 sseqtri ⊢ ( 𝑀 ... 𝑖 ) ⊆ 𝑍
153 152 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑀 ... 𝑖 ) ⊆ 𝑍 )
154 fzp1nel ⊢ ¬ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑖 )
155 154 a1i ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ¬ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑖 ) )
156 155 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ¬ ( 𝑖 + 1 ) ∈ ( 𝑀 ... 𝑖 ) )
157 129 156 eldifd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑖 + 1 ) ∈ ( 𝑍 ∖ ( 𝑀 ... 𝑖 ) ) )
158 150 153 157 106 disjiun2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅ )
159 undif4 ⊢ ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅ → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
160 158 159 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
161 160 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
162 simpl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝜑 )
163 143 128 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑖 ∈ 𝑍 )
164 112 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) ) )
165 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 = 𝑖 ) → 𝑛 = 𝑖 )
166 165 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 = 𝑖 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑖 ) )
167 166 iuneq1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑛 = 𝑖 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑗 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) )
168 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
169 ovex ⊢ ( 𝑀 ... 𝑖 ) ∈ V
170 169 131 iunex ⊢ ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∈ V
171 170 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∈ V )
172 164 167 168 171 fvmptd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑖 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) )
173 162 163 172 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝑖 ) = ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) )
174 173 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) = ( 𝐺 ‘ 𝑖 ) )
175 difid ⊢ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅
176 175 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ∅ )
177 174 176 uneq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝐺 ‘ 𝑖 ) ∪ ∅ ) )
178 un0 ⊢ ( ( 𝐺 ‘ 𝑖 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑖 )
179 178 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝑖 ) ∪ ∅ ) = ( 𝐺 ‘ 𝑖 ) )
180 177 179 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ∪ ( ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ‘ 𝑖 ) )
181 146 161 180 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) = ( 𝐺 ‘ 𝑖 ) )
182 181 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) )
183 140 182 oveq12d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
184 183 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
185 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑂 ∈ OutMeas )
186 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐸 : 𝑍 ⟶ 𝑆 )
187 186 129 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ∈ 𝑆 )
188 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝜑 )
189 92 adantr ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑀 ∈ ℤ )
190 elfzelz ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑗 ∈ ℤ )
191 190 adantl ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ ℤ )
192 elfzle1 ⊢ ( 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑀 ≤ 𝑗 )
193 192 adantl ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑀 ≤ 𝑗 )
194 189 191 193 3jca ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) )
195 eluz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗 ) )
196 194 195 sylibr ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
197 196 128 eleqtrdi ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
198 197 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
199 1 43 syl ⊢ ( 𝜑 → 𝑆 ⊆ dom 𝑂 )
200 199 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑆 ⊆ dom 𝑂 )
201 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ∈ 𝑆 )
202 200 201 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ∈ dom 𝑂 )
203 elssuni ⊢ ( ( 𝐸 ‘ 𝑗 ) ∈ dom 𝑂 → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
204 202 203 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
205 188 198 204 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
206 205 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
207 iunss ⊢ ( ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 ↔ ∀ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
208 206 207 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ∪ 𝑗 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
209 134 208 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ dom 𝑂 )
210 185 2 42 187 209 caragensplit ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) )
211 210 eqcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) )
212 211 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∩ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐺 ‘ ( 𝑖 + 1 ) ) ∖ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) ) )
213 185 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑂 ∈ OutMeas )
214 162 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝜑 )
215 elfzuz ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑀 ) )
216 215 128 eleqtrdi ⊢ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) → 𝑛 ∈ 𝑍 )
217 216 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → 𝑛 ∈ 𝑍 )
218 4 199 fssd ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ dom 𝑂 )
219 218 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ dom 𝑂 )
220 219 55 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
221 214 217 220 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝐸 ‘ 𝑛 ) ⊆ ∪ dom 𝑂 )
222 213 42 221 omecl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
223 2fveq3 ⊢ ( 𝑛 = ( 𝑖 + 1 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) )
224 143 222 223 sge0p1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
225 224 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
226 id ⊢ ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
227 226 eqcomd ⊢ ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) )
228 227 oveq1d ⊢ ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) → ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
229 228 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) )
230 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝜑 )
231 152 sseli ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑖 ) → 𝑗 ∈ 𝑍 )
232 231 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → 𝑗 ∈ 𝑍 )
233 230 232 204 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
234 233 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ) → ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
235 234 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ∀ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
236 iunss ⊢ ( ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 ↔ ∀ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
237 235 236 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ∪ 𝑗 ∈ ( 𝑀 ... 𝑖 ) ( 𝐸 ‘ 𝑗 ) ⊆ ∪ dom 𝑂 )
238 172 237 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑖 ) ⊆ ∪ dom 𝑂 )
239 162 163 238 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝑖 ) ⊆ ∪ dom 𝑂 )
240 185 42 239 omexrcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ∈ ℝ* )
241 108 208 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐸 ‘ ( 𝑖 + 1 ) ) ⊆ ∪ dom 𝑂 )
242 185 42 241 omexrcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ∈ ℝ* )
243 240 242 xaddcomd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
244 243 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) +𝑒 ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
245 225 229 244 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝑖 + 1 ) ) ) +𝑒 ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) ) )
246 184 212 245 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
247 87 88 91 246 syl3anc ⊢ ( ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) ∧ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ∧ 𝜑 ) → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
248 247 3exp ⊢ ( 𝑖 ∈ ( 𝑀 ..^ 𝑁 ) → ( ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑖 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑖 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) → ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ ( 𝑖 + 1 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... ( 𝑖 + 1 ) ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) ) )
249 16 22 28 34 86 248 fzind2 ⊢ ( 𝑁 ∈ ( 𝑀 ... 𝑁 ) → ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ) )
250 9 10 249 sylc ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐺 ‘ 𝑁 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )