Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  carageniuncllem2 Structured version   Visualization version   GIF version

Theorem carageniuncllem2 39412
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.)
Hypotheses
Ref Expression
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
Ref Expression
carageniuncllem2 (𝜑 → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) +𝑒 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ ((𝑂𝐴) + 𝑌))
Distinct variable groups:   𝐴,𝑛   𝑖,𝐸,𝑛   𝑛,𝐹   𝑖,𝑀,𝑛   𝑛,𝑂   𝑆,𝑖   𝑛,𝑋   𝑖,𝑍,𝑛   𝜑,𝑖,𝑛
Allowed substitution hints:   𝐴(𝑖)   𝑆(𝑛)   𝐹(𝑖)   𝐺(𝑖,𝑛)   𝑂(𝑖)   𝑋(𝑖)   𝑌(𝑖,𝑛)

Proof of Theorem carageniuncllem2
Dummy variables 𝑘 𝑧 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 carageniuncllem2.o . . . 4 (𝜑𝑂 ∈ OutMeas)
2 carageniuncllem2.x . . . 4 𝑋 = dom 𝑂
3 carageniuncllem2.a . . . 4 (𝜑𝐴𝑋)
4 carageniuncllem2.re . . . 4 (𝜑 → (𝑂𝐴) ∈ ℝ)
5 inss1 3795 . . . . 5 (𝐴 𝑛𝑍 (𝐸𝑛)) ⊆ 𝐴
65a1i 11 . . . 4 (𝜑 → (𝐴 𝑛𝑍 (𝐸𝑛)) ⊆ 𝐴)
71, 2, 3, 4, 6omessre 39400 . . 3 (𝜑 → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ∈ ℝ)
8 difssd 3700 . . . 4 (𝜑 → (𝐴 𝑛𝑍 (𝐸𝑛)) ⊆ 𝐴)
91, 2, 3, 4, 8omessre 39400 . . 3 (𝜑 → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ∈ ℝ)
10 rexadd 11937 . . 3 (((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ∈ ℝ ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ∈ ℝ) → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) +𝑒 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) = ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))))
117, 9, 10syl2anc 691 . 2 (𝜑 → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) +𝑒 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) = ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))))
12 carageniuncllem2.z . . . . . . . 8 𝑍 = (ℤ𝑀)
13 ssinss1 3803 . . . . . . . . . . . . 13 (𝐴𝑋 → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝑋)
143, 13syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝑋)
151, 2unidmex 38242 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ V)
16 ssexg 4732 . . . . . . . . . . . . . . 15 ((𝐴𝑋𝑋 ∈ V) → 𝐴 ∈ V)
173, 15, 16syl2anc 691 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ V)
18 inex1g 4729 . . . . . . . . . . . . . 14 (𝐴 ∈ V → (𝐴 ∩ (𝐹𝑛)) ∈ V)
1917, 18syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐴 ∩ (𝐹𝑛)) ∈ V)
20 elpwg 4116 . . . . . . . . . . . . 13 ((𝐴 ∩ (𝐹𝑛)) ∈ V → ((𝐴 ∩ (𝐹𝑛)) ∈ 𝒫 𝑋 ↔ (𝐴 ∩ (𝐹𝑛)) ⊆ 𝑋))
2119, 20syl 17 . . . . . . . . . . . 12 (𝜑 → ((𝐴 ∩ (𝐹𝑛)) ∈ 𝒫 𝑋 ↔ (𝐴 ∩ (𝐹𝑛)) ⊆ 𝑋))
2214, 21mpbird 246 . . . . . . . . . . 11 (𝜑 → (𝐴 ∩ (𝐹𝑛)) ∈ 𝒫 𝑋)
2322adantr 480 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝐴 ∩ (𝐹𝑛)) ∈ 𝒫 𝑋)
24 eqid 2610 . . . . . . . . . 10 (𝑛𝑍 ↦ (𝐴 ∩ (𝐹𝑛))) = (𝑛𝑍 ↦ (𝐴 ∩ (𝐹𝑛)))
2523, 24fmptd 6292 . . . . . . . . 9 (𝜑 → (𝑛𝑍 ↦ (𝐴 ∩ (𝐹𝑛))):𝑍⟶𝒫 𝑋)
26 fveq2 6103 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
2726ineq2d 3776 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝐴 ∩ (𝐹𝑘)) = (𝐴 ∩ (𝐹𝑛)))
2827cbvmptv 4678 . . . . . . . . . . 11 (𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘))) = (𝑛𝑍 ↦ (𝐴 ∩ (𝐹𝑛)))
2928feq1i 5949 . . . . . . . . . 10 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘))):𝑍⟶𝒫 𝑋 ↔ (𝑛𝑍 ↦ (𝐴 ∩ (𝐹𝑛))):𝑍⟶𝒫 𝑋)
3029a1i 11 . . . . . . . . 9 (𝜑 → ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘))):𝑍⟶𝒫 𝑋 ↔ (𝑛𝑍 ↦ (𝐴 ∩ (𝐹𝑛))):𝑍⟶𝒫 𝑋))
3125, 30mpbird 246 . . . . . . . 8 (𝜑 → (𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘))):𝑍⟶𝒫 𝑋)
32 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → 𝑛𝑍)
3319adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → (𝐴 ∩ (𝐹𝑛)) ∈ V)
3428fvmpt2 6200 . . . . . . . . . . . 12 ((𝑛𝑍 ∧ (𝐴 ∩ (𝐹𝑛)) ∈ V) → ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛) = (𝐴 ∩ (𝐹𝑛)))
3532, 33, 34syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛) = (𝐴 ∩ (𝐹𝑛)))
3635iuneq2dv 4478 . . . . . . . . . 10 (𝜑 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛) = 𝑛𝑍 (𝐴 ∩ (𝐹𝑛)))
3736fveq2d 6107 . . . . . . . . 9 (𝜑 → (𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) = (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))))
38 nfv 1830 . . . . . . . . . . . . . . . 16 𝑛𝜑
39 carageniuncllem2.e . . . . . . . . . . . . . . . 16 (𝜑𝐸:𝑍𝑆)
40 carageniuncllem2.f . . . . . . . . . . . . . . . 16 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑀..^𝑛)(𝐸𝑖)))
4138, 12, 39, 40iundjiun 39353 . . . . . . . . . . . . . . 15 (𝜑 → ((∀𝑚𝑍 𝑛 ∈ (𝑀...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑀...𝑚)(𝐸𝑛) ∧ 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛)) ∧ Disj 𝑛𝑍 (𝐹𝑛)))
4241simplrd 789 . . . . . . . . . . . . . 14 (𝜑 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
4342eqcomd 2616 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 (𝐸𝑛) = 𝑛𝑍 (𝐹𝑛))
4443ineq2d 3776 . . . . . . . . . . . 12 (𝜑 → (𝐴 𝑛𝑍 (𝐸𝑛)) = (𝐴 𝑛𝑍 (𝐹𝑛)))
45 iunin2 4520 . . . . . . . . . . . . . 14 𝑛𝑍 (𝐴 ∩ (𝐹𝑛)) = (𝐴 𝑛𝑍 (𝐹𝑛))
4645eqcomi 2619 . . . . . . . . . . . . 13 (𝐴 𝑛𝑍 (𝐹𝑛)) = 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))
4746a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐴 𝑛𝑍 (𝐹𝑛)) = 𝑛𝑍 (𝐴 ∩ (𝐹𝑛)))
4844, 47eqtrd 2644 . . . . . . . . . . 11 (𝜑 → (𝐴 𝑛𝑍 (𝐸𝑛)) = 𝑛𝑍 (𝐴 ∩ (𝐹𝑛)))
4948fveq2d 6107 . . . . . . . . . 10 (𝜑 → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) = (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))))
5049, 7eqeltrrd 2689 . . . . . . . . 9 (𝜑 → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
5137, 50eqeltrd 2688 . . . . . . . 8 (𝜑 → (𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) ∈ ℝ)
52 carageniuncllem2.y . . . . . . . 8 (𝜑𝑌 ∈ ℝ+)
531, 2, 12, 31, 51, 52omeiunltfirp 39409 . . . . . . 7 (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) < (Σ𝑛𝑧 (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) + 𝑌))
5437adantr 480 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) = (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))))
55 elpwinss 38241 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → 𝑧𝑍)
5655adantr 480 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛𝑧) → 𝑧𝑍)
57 simpr 476 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛𝑧) → 𝑛𝑧)
5856, 57sseldd 3569 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛𝑧) → 𝑛𝑍)
5958adantll 746 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 𝑛𝑍)
6019ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝐴 ∩ (𝐹𝑛)) ∈ V)
6159, 60, 34syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛) = (𝐴 ∩ (𝐹𝑛)))
6261fveq2d 6107 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) = (𝑂‘(𝐴 ∩ (𝐹𝑛))))
6362sumeq2dv 14281 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑛𝑧 (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) = Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))))
6463oveq1d 6564 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ𝑛𝑧 (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) + 𝑌) = (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
6554, 64breq12d 4596 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) < (Σ𝑛𝑧 (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) + 𝑌) ↔ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
6665biimpd 218 . . . . . . . 8 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) < (Σ𝑛𝑧 (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) + 𝑌) → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
6766reximdva 3000 . . . . . . 7 (𝜑 → (∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 ((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) < (Σ𝑛𝑧 (𝑂‘((𝑘𝑍 ↦ (𝐴 ∩ (𝐹𝑘)))‘𝑛)) + 𝑌) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
6853, 67mpd 15 . . . . . 6 (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
69 carageniuncllem2.m . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
7069adantr 480 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑀 ∈ ℤ)
7155adantl 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧𝑍)
72 elinel2 3762 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → 𝑧 ∈ Fin)
7372adantl 481 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ∈ Fin)
7470, 12, 71, 73uzfissfz 38483 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑘𝑍 𝑧 ⊆ (𝑀...𝑘))
7574adantr 480 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → ∃𝑘𝑍 𝑧 ⊆ (𝑀...𝑘))
7650ad3antrrr 762 . . . . . . . . . . . 12 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
77 fzfid 12634 . . . . . . . . . . . . . . . . 17 (𝑧 ⊆ (𝑀...𝑘) → (𝑀...𝑘) ∈ Fin)
78 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 ⊆ (𝑀...𝑘) → 𝑧 ⊆ (𝑀...𝑘))
79 ssfi 8065 . . . . . . . . . . . . . . . . 17 (((𝑀...𝑘) ∈ Fin ∧ 𝑧 ⊆ (𝑀...𝑘)) → 𝑧 ∈ Fin)
8077, 78, 79syl2anc 691 . . . . . . . . . . . . . . . 16 (𝑧 ⊆ (𝑀...𝑘) → 𝑧 ∈ Fin)
8180adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → 𝑧 ∈ Fin)
821ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛𝑧) → 𝑂 ∈ OutMeas)
833ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛𝑧) → 𝐴𝑋)
844ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛𝑧) → (𝑂𝐴) ∈ ℝ)
85 inss1 3795 . . . . . . . . . . . . . . . . 17 (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴
8685a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛𝑧) → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴)
8782, 2, 83, 84, 86omessre 39400 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛𝑧) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
8881, 87fsumrecl 14312 . . . . . . . . . . . . . 14 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
8952rpred 11748 . . . . . . . . . . . . . . 15 (𝜑𝑌 ∈ ℝ)
9089adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → 𝑌 ∈ ℝ)
9188, 90readdcld 9948 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) ∈ ℝ)
9291ad4ant14 1285 . . . . . . . . . . . 12 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) ∈ ℝ)
93 fzfid 12634 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀...𝑘) ∈ Fin)
9485a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∩ (𝐹𝑛)) ⊆ 𝐴)
951, 2, 3, 4, 94omessre 39400 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
9695adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑀...𝑘)) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
9793, 96fsumrecl 14312 . . . . . . . . . . . . . . 15 (𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
9897adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
9989adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑌 ∈ ℝ)
10098, 99readdcld 9948 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) ∈ ℝ)
101100ad2antrr 758 . . . . . . . . . . . 12 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) ∈ ℝ)
102 simplr 788 . . . . . . . . . . . 12 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
10397adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
104 fzfid 12634 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → (𝑀...𝑘) ∈ Fin)
10596adantlr 747 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ ℝ)
106 0xr 9965 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ*
107106a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑀...𝑘)) → 0 ∈ ℝ*)
108 pnfxr 9971 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
109108a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑀...𝑘)) → +∞ ∈ ℝ*)
1101, 2, 14omecl 39393 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ (0[,]+∞))
111110adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ (𝑀...𝑘)) → (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ (0[,]+∞))
112 iccgelb 12101 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝑂‘(𝐴 ∩ (𝐹𝑛))) ∈ (0[,]+∞)) → 0 ≤ (𝑂‘(𝐴 ∩ (𝐹𝑛))))
113107, 109, 111, 112syl3anc 1318 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (𝑀...𝑘)) → 0 ≤ (𝑂‘(𝐴 ∩ (𝐹𝑛))))
114113adantlr 747 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ (𝑀...𝑘)) → 0 ≤ (𝑂‘(𝐴 ∩ (𝐹𝑛))))
115 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → 𝑧 ⊆ (𝑀...𝑘))
116104, 105, 114, 115fsumless 14369 . . . . . . . . . . . . . 14 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) ≤ Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))))
11788, 103, 90, 116leadd1dd 10520 . . . . . . . . . . . . 13 ((𝜑𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) ≤ (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
118117ad4ant14 1285 . . . . . . . . . . . 12 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) ≤ (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
11976, 92, 101, 102, 118ltletrd 10076 . . . . . . . . . . 11 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
120119ex 449 . . . . . . . . . 10 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (𝑧 ⊆ (𝑀...𝑘) → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
121120reximdv 2999 . . . . . . . . 9 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (∃𝑘𝑍 𝑧 ⊆ (𝑀...𝑘) → ∃𝑘𝑍 (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
12275, 121mpd 15 . . . . . . . 8 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → ∃𝑘𝑍 (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
123122ex 449 . . . . . . 7 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) → ∃𝑘𝑍 (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
124123rexlimdva 3013 . . . . . 6 (𝜑 → (∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛𝑧 (𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) → ∃𝑘𝑍 (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
12568, 124mpd 15 . . . . 5 (𝜑 → ∃𝑘𝑍 (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
12649ad2antrr 758 . . . . . . . 8 (((𝜑𝑘𝑍) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) = (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))))
127 simpr 476 . . . . . . . 8 (((𝜑𝑘𝑍) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
128126, 127eqbrtrd 4605 . . . . . . 7 (((𝜑𝑘𝑍) ∧ (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
129128ex 449 . . . . . 6 ((𝜑𝑘𝑍) → ((𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
130129reximdva 3000 . . . . 5 (𝜑 → (∃𝑘𝑍 (𝑂 𝑛𝑍 (𝐴 ∩ (𝐹𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) → ∃𝑘𝑍 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)))
131125, 130mpd 15 . . . 4 (𝜑 → ∃𝑘𝑍 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
132 simpr 476 . . . . . . 7 (((𝜑𝑘𝑍) ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌))
1331adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝑂 ∈ OutMeas)
134 carageniuncllem2.s . . . . . . . . . 10 𝑆 = (CaraGen‘𝑂)
1353adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝐴𝑋)
1364adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝑂𝐴) ∈ ℝ)
13739adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝐸:𝑍𝑆)
138 carageniuncllem2.g . . . . . . . . . 10 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
139 simpr 476 . . . . . . . . . 10 ((𝜑𝑘𝑍) → 𝑘𝑍)
140133, 134, 2, 135, 136, 12, 137, 138, 40, 139carageniuncllem1 39411 . . . . . . . . 9 ((𝜑𝑘𝑍) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) = (𝑂‘(𝐴 ∩ (𝐺𝑘))))
141140oveq1d 6564 . . . . . . . 8 ((𝜑𝑘𝑍) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) = ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌))
142141adantr 480 . . . . . . 7 (((𝜑𝑘𝑍) ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) = ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌))
143132, 142breqtrd 4609 . . . . . 6 (((𝜑𝑘𝑍) ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌))
144143ex 449 . . . . 5 ((𝜑𝑘𝑍) → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)))
145144reximdva 3000 . . . 4 (𝜑 → (∃𝑘𝑍 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹𝑛))) + 𝑌) → ∃𝑘𝑍 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)))
146131, 145mpd 15 . . 3 (𝜑 → ∃𝑘𝑍 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌))
14773ad2ant1 1075 . . . . . . 7 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ∈ ℝ)
14893ad2ant1 1075 . . . . . . 7 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ∈ ℝ)
149 inss1 3795 . . . . . . . . . . 11 (𝐴 ∩ (𝐺𝑘)) ⊆ 𝐴
150149a1i 11 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝐴 ∩ (𝐺𝑘)) ⊆ 𝐴)
151133, 2, 135, 136, 150omessre 39400 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝑂‘(𝐴 ∩ (𝐺𝑘))) ∈ ℝ)
15289adantr 480 . . . . . . . . 9 ((𝜑𝑘𝑍) → 𝑌 ∈ ℝ)
153151, 152readdcld 9948 . . . . . . . 8 ((𝜑𝑘𝑍) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) ∈ ℝ)
1541533adant3 1074 . . . . . . 7 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) ∈ ℝ)
155 difssd 3700 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐴 ∖ (𝐺𝑘)) ⊆ 𝐴)
156133, 2, 135, 136, 155omessre 39400 . . . . . . . 8 ((𝜑𝑘𝑍) → (𝑂‘(𝐴 ∖ (𝐺𝑘))) ∈ ℝ)
1571563adant3 1074 . . . . . . 7 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∖ (𝐺𝑘))) ∈ ℝ)
158 simp3 1056 . . . . . . . 8 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌))
159147, 154, 158ltled 10064 . . . . . . 7 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ≤ ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌))
160135ssdifssd 3710 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐴 ∖ (𝐺𝑘)) ⊆ 𝑋)
161 oveq2 6557 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘))
162161iuneq1d 4481 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖))
163 ovex 6577 . . . . . . . . . . . . . . 15 (𝑀...𝑘) ∈ V
164 fvex 6113 . . . . . . . . . . . . . . 15 (𝐸𝑖) ∈ V
165163, 164iunex 7039 . . . . . . . . . . . . . 14 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖) ∈ V
166162, 138, 165fvmpt 6191 . . . . . . . . . . . . 13 (𝑘𝑍 → (𝐺𝑘) = 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖))
167 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 → (𝐸𝑖) = (𝐸𝑛))
168167cbviunv 4495 . . . . . . . . . . . . . 14 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖) = 𝑛 ∈ (𝑀...𝑘)(𝐸𝑛)
169168a1i 11 . . . . . . . . . . . . 13 (𝑘𝑍 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖) = 𝑛 ∈ (𝑀...𝑘)(𝐸𝑛))
170166, 169eqtrd 2644 . . . . . . . . . . . 12 (𝑘𝑍 → (𝐺𝑘) = 𝑛 ∈ (𝑀...𝑘)(𝐸𝑛))
171 elfzuz 12209 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ𝑀))
17212eqcomi 2619 . . . . . . . . . . . . . . . . 17 (ℤ𝑀) = 𝑍
173172a1i 11 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...𝑘) → (ℤ𝑀) = 𝑍)
174171, 173eleqtrd 2690 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...𝑘) → 𝑖𝑍)
175174ssriv 3572 . . . . . . . . . . . . . 14 (𝑀...𝑘) ⊆ 𝑍
176 iunss1 4468 . . . . . . . . . . . . . 14 ((𝑀...𝑘) ⊆ 𝑍 𝑛 ∈ (𝑀...𝑘)(𝐸𝑛) ⊆ 𝑛𝑍 (𝐸𝑛))
177175, 176ax-mp 5 . . . . . . . . . . . . 13 𝑛 ∈ (𝑀...𝑘)(𝐸𝑛) ⊆ 𝑛𝑍 (𝐸𝑛)
178177a1i 11 . . . . . . . . . . . 12 (𝑘𝑍 𝑛 ∈ (𝑀...𝑘)(𝐸𝑛) ⊆ 𝑛𝑍 (𝐸𝑛))
179170, 178eqsstrd 3602 . . . . . . . . . . 11 (𝑘𝑍 → (𝐺𝑘) ⊆ 𝑛𝑍 (𝐸𝑛))
180179adantl 481 . . . . . . . . . 10 ((𝜑𝑘𝑍) → (𝐺𝑘) ⊆ 𝑛𝑍 (𝐸𝑛))
181180sscond 3709 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝐴 𝑛𝑍 (𝐸𝑛)) ⊆ (𝐴 ∖ (𝐺𝑘)))
182133, 2, 160, 181omessle 39388 . . . . . . . 8 ((𝜑𝑘𝑍) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ≤ (𝑂‘(𝐴 ∖ (𝐺𝑘))))
1831823adant3 1074 . . . . . . 7 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) ≤ (𝑂‘(𝐴 ∖ (𝐺𝑘))))
184147, 148, 154, 157, 159, 183le2addd 10525 . . . . . 6 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ (((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))))
185151recnd 9947 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝑂‘(𝐴 ∩ (𝐺𝑘))) ∈ ℂ)
18689recnd 9947 . . . . . . . . . 10 (𝜑𝑌 ∈ ℂ)
187186adantr 480 . . . . . . . . 9 ((𝜑𝑘𝑍) → 𝑌 ∈ ℂ)
188156recnd 9947 . . . . . . . . 9 ((𝜑𝑘𝑍) → (𝑂‘(𝐴 ∖ (𝐺𝑘))) ∈ ℂ)
189185, 187, 188add32d 10142 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = (((𝑂‘(𝐴 ∩ (𝐺𝑘))) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) + 𝑌))
190 rexadd 11937 . . . . . . . . . . . 12 (((𝑂‘(𝐴 ∩ (𝐺𝑘))) ∈ ℝ ∧ (𝑂‘(𝐴 ∖ (𝐺𝑘))) ∈ ℝ) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))))
191151, 156, 190syl2anc 691 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))))
192191eqcomd 2616 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = ((𝑂‘(𝐴 ∩ (𝐺𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺𝑘)))))
193138a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)))
194162adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑘𝑍) ∧ 𝑛 = 𝑘) → 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖))
195 nfv 1830 . . . . . . . . . . . . . . 15 𝑖𝜑
19639adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝐸:𝑍𝑆)
197174adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀...𝑘)) → 𝑖𝑍)
198196, 197ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀...𝑘)) → (𝐸𝑖) ∈ 𝑆)
199195, 1, 134, 93, 198caragenfiiuncl 39405 . . . . . . . . . . . . . 14 (𝜑 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖) ∈ 𝑆)
200199adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑘𝑍) → 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖) ∈ 𝑆)
201193, 194, 139, 200fvmptd 6197 . . . . . . . . . . . 12 ((𝜑𝑘𝑍) → (𝐺𝑘) = 𝑖 ∈ (𝑀...𝑘)(𝐸𝑖))
202201, 200eqeltrd 2688 . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐺𝑘) ∈ 𝑆)
203133, 134, 2, 202, 135caragensplit 39390 . . . . . . . . . 10 ((𝜑𝑘𝑍) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = (𝑂𝐴))
204192, 203eqtrd 2644 . . . . . . . . 9 ((𝜑𝑘𝑍) → ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = (𝑂𝐴))
205204oveq1d 6564 . . . . . . . 8 ((𝜑𝑘𝑍) → (((𝑂‘(𝐴 ∩ (𝐺𝑘))) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) + 𝑌) = ((𝑂𝐴) + 𝑌))
206189, 205eqtrd 2644 . . . . . . 7 ((𝜑𝑘𝑍) → (((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = ((𝑂𝐴) + 𝑌))
2072063adant3 1074 . . . . . 6 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → (((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺𝑘)))) = ((𝑂𝐴) + 𝑌))
208184, 207breqtrd 4609 . . . . 5 ((𝜑𝑘𝑍 ∧ (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌)) → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ ((𝑂𝐴) + 𝑌))
2092083exp 1256 . . . 4 (𝜑 → (𝑘𝑍 → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ ((𝑂𝐴) + 𝑌))))
210209rexlimdv 3012 . . 3 (𝜑 → (∃𝑘𝑍 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺𝑘))) + 𝑌) → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ ((𝑂𝐴) + 𝑌)))
211146, 210mpd 15 . 2 (𝜑 → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) + (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ ((𝑂𝐴) + 𝑌))
21211, 211eqbrtrd 4605 1 (𝜑 → ((𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛))) +𝑒 (𝑂‘(𝐴 𝑛𝑍 (𝐸𝑛)))) ≤ ((𝑂𝐴) + 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wral 2896  wrex 2897  Vcvv 3173  cdif 3537  cin 3539  wss 3540  𝒫 cpw 4108   cuni 4372   ciun 4455  Disj wdisj 4553   class class class wbr 4583  cmpt 4643  dom cdm 5038  wf 5800  cfv 5804  (class class class)co 6549  Fincfn 7841  cc 9813  cr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  *cxr 9952   < clt 9953  cle 9954  cz 11254  cuz 11563  +crp 11708   +𝑒 cxad 11820  [,]cicc 12049  ...cfz 12197  ..^cfzo 12334  Σcsu 14264  OutMeascome 39379  CaraGenccaragen 39381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-ac2 9168  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-disj 4554  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-omul 7452  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-acn 8651  df-ac 8822  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-xadd 11823  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-sumge0 39256  df-ome 39380  df-caragen 39382
This theorem is referenced by:  carageniuncl  39413
  Copyright terms: Public domain W3C validator