Metamath Proof Explorer

Theorem carageniuncllem2

Description: The Caratheodory's construction is closed under countable union. Step (d) in the proof of Theorem 113C of Fremlin1 p. 20. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 carageniuncllem2.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2 carageniuncllem2.s ⊢ 𝑆 = ( CaraGen ‘ 𝑂 )
3 carageniuncllem2.x ⊢ 𝑋 = ∪ dom 𝑂
4 carageniuncllem2.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
5 carageniuncllem2.re ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
6 carageniuncllem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7 carageniuncllem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
8 carageniuncllem2.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝑆 )
9 carageniuncllem2.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ+ )
10 carageniuncllem2.g ⊢ 𝐺 = ( 𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) )
11 carageniuncllem2.f ⊢ 𝐹 = ( 𝑛 ∈ 𝑍 ↦ ( ( 𝐸 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 𝑀 ..^ 𝑛 ) ( 𝐸 ‘ 𝑖 ) ) )
12 inss1 ⊢ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ 𝐴
13 12 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ 𝐴 )
14 1 3 4 5 13 omessre ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ )
15 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ 𝐴 )
16 1 3 4 5 15 omessre ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ )
17 rexadd ⊢ ( ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ ∧ ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) )
18 14 16 17 syl2anc ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) )
19 ssinss1 ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑋 )
20 4 19 syl ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑋 )
21 1 3 unidmex ⊢ ( 𝜑 → 𝑋 ∈ V )
22 ssexg ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ V ) → 𝐴 ∈ V )
23 4 21 22 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ V )
24 inex1g ⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
25 23 24 syl ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
26 elpwg ⊢ ( ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ V → ( ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝒫 𝑋 ↔ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑋 ) )
27 25 26 syl ⊢ ( 𝜑 → ( ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝒫 𝑋 ↔ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝑋 ) )
28 20 27 mpbird ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝒫 𝑋 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ 𝒫 𝑋 )
30 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
31 29 30 fmptd ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) : 𝑍 ⟶ 𝒫 𝑋 )
32 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
33 32 ineq2d ⊢ ( 𝑘 = 𝑛 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
34 33 cbvmptv ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
35 34 feq1i ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ 𝒫 𝑋 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) : 𝑍 ⟶ 𝒫 𝑋 )
36 35 a1i ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ 𝒫 𝑋 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) : 𝑍 ⟶ 𝒫 𝑋 ) )
37 31 36 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) : 𝑍 ⟶ 𝒫 𝑋 )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
39 25 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
40 34 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
41 38 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
42 41 iuneq2dv ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
43 42 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
44 nfv ⊢ Ⅎ 𝑛 𝜑
45 44 7 8 11 iundjiun ⊢ ( 𝜑 → ( ( ∀ 𝑚 ∈ 𝑍 ∪ 𝑛 ∈ ( 𝑀 ... 𝑚 ) ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ ( 𝑀 ... 𝑚 ) ( 𝐸 ‘ 𝑛 ) ∧ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∧ Disj 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) )
46 45 simplrd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
47 46 eqcomd ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) )
48 47 ineq2d ⊢ ( 𝜑 → ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) )
49 iunin2 ⊢ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) )
50 49 eqcomi ⊢ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) = ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) )
51 50 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ) = ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
52 48 51 eqtrd ⊢ ( 𝜑 → ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
53 52 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
54 53 14 eqeltrrd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
55 43 54 eqeltrd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) ∈ ℝ )
56 1 3 7 37 55 9 omeiunltfirp ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) + 𝑌 ) )
57 43 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
58 elpwinss ⊢ ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑧 ⊆ 𝑍 )
59 58 adantr ⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑛 ∈ 𝑧 ) → 𝑧 ⊆ 𝑍 )
60 simpr ⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑛 ∈ 𝑧 ) → 𝑛 ∈ 𝑧 )
61 59 60 sseldd ⊢ ( ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ∧ 𝑛 ∈ 𝑧 ) → 𝑛 ∈ 𝑍 )
62 61 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → 𝑛 ∈ 𝑍 )
63 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ∈ V )
64 62 63 40 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) )
65 64 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
66 65 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) = Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
67 66 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) + 𝑌 ) = ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
68 57 67 breq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) + 𝑌 ) ↔ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
69 68 biimpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) + 𝑌 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
70 69 reximdva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐴 ∩ ( 𝐹 ‘ 𝑘 ) ) ) ‘ 𝑛 ) ) + 𝑌 ) → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
71 56 70 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
72 6 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑀 ∈ ℤ )
73 58 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑧 ⊆ 𝑍 )
74 elinel2 ⊢ ( 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) → 𝑧 ∈ Fin )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑧 ∈ Fin )
76 72 7 73 75 uzfissfz ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ∃ 𝑘 ∈ 𝑍 𝑧 ⊆ ( 𝑀 ... 𝑘 ) )
77 76 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ∃ 𝑘 ∈ 𝑍 𝑧 ⊆ ( 𝑀 ... 𝑘 ) )
78 54 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
79 fzfid ⊢ ( 𝑧 ⊆ ( 𝑀 ... 𝑘 ) → ( 𝑀 ... 𝑘 ) ∈ Fin )
80 id ⊢ ( 𝑧 ⊆ ( 𝑀 ... 𝑘 ) → 𝑧 ⊆ ( 𝑀 ... 𝑘 ) )
81 ssfi ⊢ ( ( ( 𝑀 ... 𝑘 ) ∈ Fin ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → 𝑧 ∈ Fin )
82 79 80 81 syl2anc ⊢ ( 𝑧 ⊆ ( 𝑀 ... 𝑘 ) → 𝑧 ∈ Fin )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → 𝑧 ∈ Fin )
84 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑧 ) → 𝑂 ∈ OutMeas )
85 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑧 ) → 𝐴 ⊆ 𝑋 )
86 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
87 inss1 ⊢ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝐴
88 87 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝐴 )
89 84 3 85 86 88 omessre ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ 𝑧 ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
90 83 89 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
91 9 rpred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → 𝑌 ∈ ℝ )
93 90 92 readdcld ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ∈ ℝ )
94 93 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ∈ ℝ )
95 fzfid ⊢ ( 𝜑 → ( 𝑀 ... 𝑘 ) ∈ Fin )
96 87 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ⊆ 𝐴 )
97 1 3 4 5 96 omessre ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
99 95 98 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
101 91 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → 𝑌 ∈ ℝ )
102 100 101 readdcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ∈ ℝ )
103 102 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ∈ ℝ )
104 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
105 99 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
106 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( 𝑀 ... 𝑘 ) ∈ Fin )
107 98 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ℝ )
108 0xr ⊢ 0 ∈ ℝ*
109 108 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → 0 ∈ ℝ* )
110 pnfxr ⊢ +∞ ∈ ℝ*
111 110 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → +∞ ∈ ℝ* )
112 1 3 20 omecl ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) )
114 iccgelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
115 109 111 113 114 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → 0 ≤ ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
116 115 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) ∧ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ) → 0 ≤ ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
117 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → 𝑧 ⊆ ( 𝑀 ... 𝑘 ) )
118 106 107 116 117 fsumless ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
119 90 105 92 118 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ≤ ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
120 119 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ≤ ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
121 78 94 103 104 120 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) ∧ 𝑧 ⊆ ( 𝑀 ... 𝑘 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
122 121 ex ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( 𝑧 ⊆ ( 𝑀 ... 𝑘 ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
123 122 reximdv ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( ∃ 𝑘 ∈ 𝑍 𝑧 ⊆ ( 𝑀 ... 𝑘 ) → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
124 77 123 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
125 124 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝒫 𝑍 ∩ Fin ) ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ 𝑧 ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
126 71 125 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
127 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) )
128 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
129 127 128 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
130 129 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
131 130 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) )
132 126 131 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
133 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) )
134 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑂 ∈ OutMeas )
135 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ⊆ 𝑋 )
136 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℝ )
137 8 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐸 : 𝑍 ⟶ 𝑆 )
138 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
139 134 2 3 135 136 7 137 10 11 138 carageniuncllem1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) = ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) )
140 139 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) )
142 133 141 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) )
143 142 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) )
144 143 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐹 ‘ 𝑛 ) ) ) + 𝑌 ) → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) )
145 132 144 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) )
146 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ )
147 16 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ∈ ℝ )
148 inss1 ⊢ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ⊆ 𝐴
149 148 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ⊆ 𝐴 )
150 134 3 135 136 149 omessre ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℝ )
151 91 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑌 ∈ ℝ )
152 150 151 readdcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ∈ ℝ )
153 152 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ∈ ℝ )
154 difssd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ⊆ 𝐴 )
155 134 3 135 136 154 omessre ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℝ )
156 155 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℝ )
157 simp3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) )
158 146 153 157 ltled ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ≤ ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) )
159 135 ssdifssd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ⊆ 𝑋 )
160 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑘 ) )
161 160 iuneq1d ⊢ ( 𝑛 = 𝑘 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑛 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) )
162 ovex ⊢ ( 𝑀 ... 𝑘 ) ∈ V
163 fvex ⊢ ( 𝐸 ‘ 𝑖 ) ∈ V
164 162 163 iunex ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) ∈ V
165 161 10 164 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐺 ‘ 𝑘 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) )
166 fveq2 ⊢ ( 𝑖 = 𝑛 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑛 ) )
167 166 cbviunv ⊢ ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑛 )
168 167 a1i ⊢ ( 𝑘 ∈ 𝑍 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) = ∪ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) )
169 165 168 eqtrd ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐺 ‘ 𝑘 ) = ∪ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) )
170 elfzuz ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ∈ ( ℤ≥ ‘ 𝑀 ) )
171 7 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
172 171 a1i ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → ( ℤ≥ ‘ 𝑀 ) = 𝑍 )
173 170 172 eleqtrd ⊢ ( 𝑖 ∈ ( 𝑀 ... 𝑘 ) → 𝑖 ∈ 𝑍 )
174 173 ssriv ⊢ ( 𝑀 ... 𝑘 ) ⊆ 𝑍
175 iunss1 ⊢ ( ( 𝑀 ... 𝑘 ) ⊆ 𝑍 → ∪ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
176 174 175 ax-mp ⊢ ∪ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 )
177 176 a1i ⊢ ( 𝑘 ∈ 𝑍 → ∪ 𝑛 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑛 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
178 169 177 eqsstrd ⊢ ( 𝑘 ∈ 𝑍 → ( 𝐺 ‘ 𝑘 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
179 178 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ⊆ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) )
180 179 sscond ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ⊆ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) )
181 134 3 159 180 omessle ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ≤ ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) )
182 181 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ≤ ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) )
183 146 147 153 156 158 182 le2addd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) )
184 150 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℂ )
185 91 recnd ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
186 185 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑌 ∈ ℂ )
187 155 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℂ )
188 184 186 187 add32d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) + 𝑌 ) )
189 rexadd ⊢ ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℝ ∧ ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ∈ ℝ ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) )
190 150 155 189 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) )
191 190 eqcomd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) )
192 nfv ⊢ Ⅎ 𝑖 𝜑
193 8 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝐸 : 𝑍 ⟶ 𝑆 )
194 173 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → 𝑖 ∈ 𝑍 )
195 193 194 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ) → ( 𝐸 ‘ 𝑖 ) ∈ 𝑆 )
196 192 1 2 95 195 caragenfiiuncl ⊢ ( 𝜑 → ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) ∈ 𝑆 )
197 196 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) ∈ 𝑆 )
198 10 161 138 197 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = ∪ 𝑖 ∈ ( 𝑀 ... 𝑘 ) ( 𝐸 ‘ 𝑖 ) )
199 198 197 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑆 )
200 134 2 3 199 135 caragensplit ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( 𝑂 ‘ 𝐴 ) )
201 191 200 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( 𝑂 ‘ 𝐴 ) )
202 201 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) + 𝑌 ) = ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) )
203 188 202 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) )
204 203 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) + ( 𝑂 ‘ ( 𝐴 ∖ ( 𝐺 ‘ 𝑘 ) ) ) ) = ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) )
205 183 204 breqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ∧ ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) )
206 205 3exp ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) ) ) )
207 206 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) < ( ( 𝑂 ‘ ( 𝐴 ∩ ( 𝐺 ‘ 𝑘 ) ) ) + 𝑌 ) → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) ) )
208 145 207 mpd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) + ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) )
209 18 208 eqbrtrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝐴 ∩ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) +e ( 𝑂 ‘ ( 𝐴 ∖ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ) ) ≤ ( ( 𝑂 ‘ 𝐴 ) + 𝑌 ) )