Metamath Proof Explorer

Theorem carageniuncllem1

Description: The outer measure of A i^i ( Gn ) is the sum of the outer measures of A i^i ( Fm ) . These are lines 7 to 10 of Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses carageniuncllem1.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
carageniuncllem1.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
carageniuncllem1.x ⊢ 𝑋 = ∪ dom 𝑂
carageniuncllem1.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
carageniuncllem1.re ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
carageniuncllem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
carageniuncllem1.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
carageniuncllem1.g ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
carageniuncllem1.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
carageniuncllem1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
Assertion carageniuncllem1 ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝐾 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 carageniuncllem1.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 carageniuncllem1.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 carageniuncllem1.x ⊢ 𝑋 = ∪ dom 𝑂
4 carageniuncllem1.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
5 carageniuncllem1.re ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
6 carageniuncllem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
7 carageniuncllem1.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
8 carageniuncllem1.g ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
9 carageniuncllem1.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
10 carageniuncllem1.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑍 )
11 10 6 eleqtrdi ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
12 eluzfz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ( 𝑀 ... 𝐾 ) )
13 11 12 syl ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝐾 ) )
14 id ⊢ ( 𝜑 → 𝜑 )
15 oveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑀 ) )
16 15 sumeq1d ⊢ ( 𝑘 = 𝑀 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 𝑀 ... 𝑀 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
17 fveq2 ⊢ ( 𝑘 = 𝑀 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑀 ) )
18 17 ineq2d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) )
19 18 fveq2d ⊢ ( 𝑘 = 𝑀 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) )
20 16 19 eqeq12d ⊢ ( 𝑘 = 𝑀 → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ↔ Σ 𝑛 ∈ ( 𝑀 ... 𝑀 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) ) )
21 20 imbi2d ⊢ ( 𝑘 = 𝑀 → ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑀 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) ) ) )
22 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝑗 ) )
23 22 sumeq1d ⊢ ( 𝑘 = 𝑗 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
24 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝑗 ) )
25 24 ineq2d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) )
26 25 fveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) )
27 23 26 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ↔ Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) )
28 27 imbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) ) )
29 oveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... ( 𝑗 + 1 ) ) )
30 29 sumeq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
31 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
32 31 ineq2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) )
33 32 fveq2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) )
34 30 33 eqeq12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ↔ Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) ) )
35 34 imbi2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
36 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑀 ... 𝑘 ) = ( 𝑀 ... 𝐾 ) )
37 36 sumeq1d ⊢ ( 𝑘 = 𝐾 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 𝑀 ... 𝐾 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
38 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 𝐾 ) )
39 38 ineq2d ⊢ ( 𝑘 = 𝐾 → ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) )
40 39 fveq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) ) )
41 37 40 eqeq12d ⊢ ( 𝑘 = 𝐾 → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ↔ Σ 𝑛 ∈ ( 𝑀 ... 𝐾 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) ) ) )
42 41 imbi2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ) ↔ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝐾 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) ) ) ) )
43 eluzel2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
44 11 43 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
45 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
46 44 45 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
47 46 sumeq1d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑀 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ { 𝑀 } ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
48 inss1 ⊢ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ⊆ 𝐴
49 48 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ⊆ 𝐴 )
50 1 3 4 5 49 omessre ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) ∈ ℝ )
51 50 recnd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) ∈ ℂ )
52 fveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑀 ) )
53 52 ineq2d ⊢ ( 𝑛 = 𝑀 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) )
54 53 fveq2d ⊢ ( 𝑛 = 𝑀 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) )
55 54 sumsn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) ∈ ℂ ) → Σ 𝑛 ∈ { 𝑀 } ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) )
56 44 51 55 syl2anc ⊢ ( 𝜑 → Σ 𝑛 ∈ { 𝑀 } ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) )
57 eqidd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ‘ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ‘ 𝑀 ) ) ) )
58 fveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ 𝑀 ) )
59 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑀 ..^ 𝑛 ) = ( 𝑀 ..^ 𝑀 ) )
60 59 iuneq1d ⊢ ( 𝑛 = 𝑀 → ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
61 58 60 difeq12d ⊢ ( 𝑛 = 𝑀 → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) )
62 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
63 44 62 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
64 6 a1i ⊢ ( 𝜑 → 𝑍 = ( ℤ≥ ‘ 𝑀 ) )
65 64 eqcomd ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑀 ) = 𝑍 )
66 63 65 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
67 fvex ⊢ ( 𝐸 ‘ 𝑀 ) ∈ V
68 difexg ⊢ ( ( 𝐸 ‘ 𝑀 ) ∈ V → ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V )
69 67 68 ax-mp ⊢ ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V
70 69 a1i ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) ∈ V )
71 9 61 66 70 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) )
72 fzo0 ⊢ ( 𝑀 ..^ 𝑀 ) = ∅
73 iuneq1 ⊢ ( ( 𝑀 ..^ 𝑀 ) = ∅ → ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ∅ ( 𝐸 ‘ 𝑖 ) )
74 72 73 ax-mp ⊢ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ∅ ( 𝐸 ‘ 𝑖 )
75 0iun ⊢ ∪ 𝑖 ∈ ∅ ( 𝐸 ‘ 𝑖 ) = ∅
76 74 75 eqtri ⊢ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) = ∅
77 76 difeq2i ⊢ ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝑀 ) ∖ ∅ )
78 77 a1i ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑀 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑀 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ 𝑀 ) ∖ ∅ ) )
79 dif0 ⊢ ( ( 𝐸 ‘ 𝑀 ) ∖ ∅ ) = ( 𝐸 ‘ 𝑀 )
80 79 a1i ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑀 ) ∖ ∅ ) = ( 𝐸 ‘ 𝑀 ) )
81 71 78 80 3eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( 𝐸 ‘ 𝑀 ) )
82 81 ineq2d ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) = ( 𝐴 ∩ ( 𝐸 ‘ 𝑀 ) ) )
83 82 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ‘ 𝑀 ) ) ) )
84 oveq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑀 ) )
85 84 iuneq1d ⊢ ( 𝑛 = 𝑀 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
86 ovex ⊢ ( 𝑀 ... 𝑀 ) ∈ V
87 fvex ⊢ ( 𝐸 ‘ 𝑖 ) ∈ V
88 86 87 iunex ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) ∈ V
89 88 a1i ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) ∈ V )
90 8 85 66 89 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) )
91 46 iuneq1d ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑀 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ { 𝑀 } ( 𝐸 ‘ 𝑖 ) )
92 fveq2 ⊢ ( 𝑖 = 𝑀 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑀 ) )
93 92 iunxsng ⊢ ( 𝑀 ∈ ℤ → ∪ 𝑖 ∈ { 𝑀 } ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑀 ) )
94 44 93 syl ⊢ ( 𝜑 → ∪ 𝑖 ∈ { 𝑀 } ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑀 ) )
95 90 91 94 3eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑀 ) = ( 𝐸 ‘ 𝑀 ) )
96 95 ineq2d ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) = ( 𝐴 ∩ ( 𝐸 ‘ 𝑀 ) ) )
97 96 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐸 ‘ 𝑀 ) ) ) )
98 57 83 97 3eqtr4d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑀 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) )
99 47 56 98 3eqtrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑀 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) )
100 99 a1i ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑀 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑀 ) ) ) ) )
101 simp3 ⊢ ( ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ 𝜑 ) → 𝜑 )
102 simp1 ⊢ ( ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ 𝜑 ) → 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) )
103 id ⊢ ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) )
104 103 imp ⊢ ( ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ 𝜑 ) → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) )
105 104 3adant1 ⊢ ( ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ 𝜑 ) → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) )
106 elfzouz ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
108 1 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → 𝑂 ∈ OutMeas )
109 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → 𝐴 ⊆ 𝑋 )
110 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
111 inss1 ⊢ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝐴
112 111 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝐴 )
113 108 3 109 110 112 omessre ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
114 113 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℂ )
115 114 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) ∧ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℂ )
116 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
117 116 ineq2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
118 117 fveq2d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) )
119 107 115 118 fsump1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
120 119 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) → Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
121 oveq1 ⊢ ( Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
122 121 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) )
123 fzssp1 ⊢ ( 𝑀 ... 𝑗 ) ⊆ ( 𝑀 ... ( 𝑗 + 1 ) )
124 iunss1 ⊢ ( ( 𝑀 ... 𝑗 ) ⊆ ( 𝑀 ... ( 𝑗 + 1 ) ) → ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ⊆ ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) )
125 123 124 ax-mp ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ⊆ ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 )
126 125 a1i ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ⊆ ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) )
127 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑗 ) )
128 127 iuneq1d ⊢ ( 𝑛 = 𝑗 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) )
129 106 6 eleqtrrdi ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → 𝑗 ∈ 𝑍 )
130 ovex ⊢ ( 𝑀 ... 𝑗 ) ∈ V
131 130 87 iunex ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∈ V
132 131 a1i ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∈ V )
133 8 128 129 132 fvmptd3 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝐺 ‘ 𝑗 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) )
134 oveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... ( 𝑗 + 1 ) ) )
135 134 iuneq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) )
136 peano2uz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
137 106 136 syl ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
138 6 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
139 137 138 eleqtrdi ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝑗 + 1 ) ∈ 𝑍 )
140 ovex ⊢ ( 𝑀 ... ( 𝑗 + 1 ) ) ∈ V
141 140 87 iunex ⊢ ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ∈ V
142 141 a1i ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ∈ V )
143 8 135 139 142 fvmptd3 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) )
144 133 143 sseq12d ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝐺 ‘ 𝑗 ) ⊆ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ↔ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ⊆ ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) )
145 126 144 mpbird ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝐺 ‘ 𝑗 ) ⊆ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
146 inabs3 ⊢ ( ( 𝐺 ‘ 𝑗 ) ⊆ ( 𝐺 ‘ ( 𝑗 + 1 ) ) → ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) = ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) )
147 145 146 syl ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) = ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) )
148 147 fveq2d ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) )
149 148 eqcomd ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) = ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) )
150 149 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) = ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) )
151 elfzoelz ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → 𝑗 ∈ ℤ )
152 fzval3 ⊢ ( 𝑗 ∈ ℤ → ( 𝑀 ... 𝑗 ) = ( 𝑀 ..^ ( 𝑗 + 1 ) ) )
153 151 152 syl ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝑀 ... 𝑗 ) = ( 𝑀 ..^ ( 𝑗 + 1 ) ) )
154 153 eqcomd ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝑀 ..^ ( 𝑗 + 1 ) ) = ( 𝑀 ... 𝑗 ) )
155 154 iuneq1d ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) )
156 155 difeq2d ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
157 156 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
158 fveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝐸 ‘ 𝑛 ) = ( 𝐸 ‘ ( 𝑗 + 1 ) ) )
159 oveq2 ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( 𝑀 ..^ 𝑛 ) = ( 𝑀 ..^ ( 𝑗 + 1 ) ) )
160 159 iuneq1d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) )
161 158 160 difeq12d ⊢ ( 𝑛 = ( 𝑗 + 1 ) → ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) )
162 fvex ⊢ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∈ V
163 difexg ⊢ ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∈ V → ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) ∈ V )
164 162 163 ax-mp ⊢ ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) ∈ V
165 164 a1i ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) ∈ V )
166 9 161 139 165 fvmptd3 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) )
167 166 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) ) )
168 nfcv ⊢ Ⅎ 𝑖 ( 𝐸 ‘ ( 𝑗 + 1 ) )
169 fveq2 ⊢ ( 𝑖 = ( 𝑗 + 1 ) → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ ( 𝑗 + 1 ) ) )
170 168 106 169 iunp1 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ∪ 𝑖 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝐸 ‘ 𝑖 ) = ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∪ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ) )
171 143 170 eqtrd ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∪ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ) )
172 171 133 difeq12d ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) = ( ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∪ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
173 difundir ⊢ ( ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∪ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) ∪ ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
174 difid ⊢ ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) = ∅
175 174 uneq1i ⊢ ( ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) ∪ ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) ) = ( ∅ ∪ ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
176 0un ⊢ ( ∅ ∪ ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) )
177 173 175 176 3eqtri ⊢ ( ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∪ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) )
178 177 a1i ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∪ ( 𝐸 ‘ ( 𝑗 + 1 ) ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
179 172 178 eqtrd ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
180 179 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) = ( ( 𝐸 ‘ ( 𝑗 + 1 ) ) ∖ ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ) )
181 157 167 180 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) = ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) )
182 181 ineq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( 𝐴 ∩ ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) )
183 indif2 ⊢ ( 𝐴 ∩ ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) = ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) )
184 183 eqcomi ⊢ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) = ( 𝐴 ∩ ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) )
185 184 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) = ( 𝐴 ∩ ( ( 𝐺 ‘ ( 𝑗 + 1 ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) )
186 182 185 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) )
187 186 fveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) )
188 150 187 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) )
189 inss1 ⊢ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ⊆ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
190 inss1 ⊢ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ⊆ 𝐴
191 189 190 sstri ⊢ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ⊆ 𝐴
192 191 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ⊆ 𝐴 )
193 1 3 4 5 192 omessre ⊢ ( 𝜑 → ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
194 193 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
195 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → 𝑂 ∈ OutMeas )
196 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → 𝐴 ⊆ 𝑋 )
197 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
198 difss ⊢ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ⊆ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
199 198 190 sstri ⊢ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ⊆ 𝐴
200 199 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ⊆ 𝐴 )
201 195 3 196 197 200 omessre ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ )
202 rexadd ⊢ ( ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ∧ ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ∈ ℝ ) → ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) )
203 194 201 202 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) )
204 203 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) )
205 133 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐺 ‘ 𝑗 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) )
206 nfv ⊢ Ⅎ 𝑖 𝜑
207 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑗 ) ∈ Fin )
208 7 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ) → 𝐸 : 𝑍 ⟶ 𝑆 )
209 elfzuz ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑗 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
210 138 a1i ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑗 ) → ( ℤ≥ ‘ 𝑀 ) = 𝑍 )
211 209 210 eleqtrd ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑗 ) → 𝑖 ∈ 𝑍 )
212 211 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ) → 𝑖 ∈ 𝑍 )
213 208 212 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐸 ‘ 𝑖 ) ∈ 𝑆 )
214 206 1 2 207 213 caragenfiiuncl ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∈ 𝑆 )
215 214 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ∪ 𝑖 ∈ ( 𝑀 ... 𝑗 ) ( 𝐸 ‘ 𝑖 ) ∈ 𝑆 )
216 205 215 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐺 ‘ 𝑗 ) ∈ 𝑆 )
217 4 ssinss1d ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ⊆ 𝑋 )
218 217 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ⊆ 𝑋 )
219 195 2 3 216 218 caragensplit ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∩ ( 𝐺 ‘ 𝑗 ) ) ) +𝑒 ( 𝑂 ‘ ( ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ∖ ( 𝐺 ‘ 𝑗 ) ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) )
220 188 204 219 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) )
221 220 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) )
222 120 122 221 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) → Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) )
223 101 102 105 222 syl3anc ⊢ ( ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) ∧ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) ∧ 𝜑 ) → Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) )
224 223 3exp ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝐾 ) → ( ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑗 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑗 ) ) ) ) → ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ ( 𝑗 + 1 ) ) ) ) ) ) )
225 21 28 35 42 100 224 fzind2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝐾 ) → ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝐾 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) ) ) )
226 13 14 225 sylc ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝐾 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝐾 ) ) ) )