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 45238
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 4229 . . . . 5 (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) βŠ† 𝐴
65a1i 11 . . . 4 (πœ‘ β†’ (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) βŠ† 𝐴)
71, 2, 3, 4, 6omessre 45226 . . 3 (πœ‘ β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ∈ ℝ)
8 difssd 4133 . . . 4 (πœ‘ β†’ (𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) βŠ† 𝐴)
91, 2, 3, 4, 8omessre 45226 . . 3 (πœ‘ β†’ (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ∈ ℝ)
10 rexadd 13211 . . 3 (((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ∈ ℝ ∧ (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ∈ ℝ) β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) +𝑒 (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) = ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))))
117, 9, 10syl2anc 585 . 2 (πœ‘ β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) +𝑒 (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) = ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))))
12 carageniuncllem2.z . . . . . . . 8 𝑍 = (β„€β‰₯β€˜π‘€)
13 ssinss1 4238 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝑋 β†’ (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝑋)
143, 13syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝑋)
151, 2unidmex 43737 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑋 ∈ V)
16 ssexg 5324 . . . . . . . . . . . . . . 15 ((𝐴 βŠ† 𝑋 ∧ 𝑋 ∈ V) β†’ 𝐴 ∈ V)
173, 15, 16syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 ∈ V)
18 inex1g 5320 . . . . . . . . . . . . . 14 (𝐴 ∈ V β†’ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ V)
1917, 18syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ V)
20 elpwg 4606 . . . . . . . . . . . . 13 ((𝐴 ∩ (πΉβ€˜π‘›)) ∈ V β†’ ((𝐴 ∩ (πΉβ€˜π‘›)) ∈ 𝒫 𝑋 ↔ (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝑋))
2119, 20syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐴 ∩ (πΉβ€˜π‘›)) ∈ 𝒫 𝑋 ↔ (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝑋))
2214, 21mpbird 257 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ 𝒫 𝑋)
2322adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ 𝒫 𝑋)
24 eqid 2733 . . . . . . . . . 10 (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘›))) = (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘›)))
2523, 24fmptd 7114 . . . . . . . . 9 (πœ‘ β†’ (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘›))):π‘βŸΆπ’« 𝑋)
26 fveq2 6892 . . . . . . . . . . . . 13 (π‘˜ = 𝑛 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘›))
2726ineq2d 4213 . . . . . . . . . . . 12 (π‘˜ = 𝑛 β†’ (𝐴 ∩ (πΉβ€˜π‘˜)) = (𝐴 ∩ (πΉβ€˜π‘›)))
2827cbvmptv 5262 . . . . . . . . . . 11 (π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜))) = (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘›)))
2928feq1i 6709 . . . . . . . . . 10 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜))):π‘βŸΆπ’« 𝑋 ↔ (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘›))):π‘βŸΆπ’« 𝑋)
3029a1i 11 . . . . . . . . 9 (πœ‘ β†’ ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜))):π‘βŸΆπ’« 𝑋 ↔ (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘›))):π‘βŸΆπ’« 𝑋))
3125, 30mpbird 257 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜))):π‘βŸΆπ’« 𝑋)
32 simpr 486 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ 𝑛 ∈ 𝑍)
3319adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ V)
3428fvmpt2 7010 . . . . . . . . . . . 12 ((𝑛 ∈ 𝑍 ∧ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ V) β†’ ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›) = (𝐴 ∩ (πΉβ€˜π‘›)))
3532, 33, 34syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›) = (𝐴 ∩ (πΉβ€˜π‘›)))
3635iuneq2dv 5022 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›) = βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›)))
3736fveq2d 6896 . . . . . . . . 9 (πœ‘ β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) = (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))))
38 nfv 1918 . . . . . . . . . . . . . . . 16 β„²π‘›πœ‘
39 carageniuncllem2.e . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐸:π‘βŸΆπ‘†)
40 carageniuncllem2.f . . . . . . . . . . . . . . . 16 𝐹 = (𝑛 ∈ 𝑍 ↦ ((πΈβ€˜π‘›) βˆ– βˆͺ 𝑖 ∈ (𝑀..^𝑛)(πΈβ€˜π‘–)))
4138, 12, 39, 40iundjiun 45176 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((βˆ€π‘š ∈ 𝑍 βˆͺ 𝑛 ∈ (𝑀...π‘š)(πΉβ€˜π‘›) = βˆͺ 𝑛 ∈ (𝑀...π‘š)(πΈβ€˜π‘›) ∧ βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›) = βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) ∧ Disj 𝑛 ∈ 𝑍 (πΉβ€˜π‘›)))
4241simplrd 769 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›) = βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))
4342eqcomd 2739 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›) = βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›))
4443ineq2d 4213 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) = (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›)))
45 iunin2 5075 . . . . . . . . . . . . . 14 βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›)) = (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›))
4645eqcomi 2742 . . . . . . . . . . . . 13 (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›)) = βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))
4746a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΉβ€˜π‘›)) = βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›)))
4844, 47eqtrd 2773 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) = βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›)))
4948fveq2d 6896 . . . . . . . . . 10 (πœ‘ β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) = (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))))
5049, 7eqeltrrd 2835 . . . . . . . . 9 (πœ‘ β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
5137, 50eqeltrd 2834 . . . . . . . 8 (πœ‘ β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) ∈ ℝ)
52 carageniuncllem2.y . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ ℝ+)
531, 2, 12, 31, 51, 52omeiunltfirp 45235 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘§ ∈ (𝒫 𝑍 ∩ Fin)(π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) + π‘Œ))
5437adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) = (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))))
55 elpwinss 43736 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) β†’ 𝑧 βŠ† 𝑍)
5655adantr 482 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛 ∈ 𝑧) β†’ 𝑧 βŠ† 𝑍)
57 simpr 486 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛 ∈ 𝑧) β†’ 𝑛 ∈ 𝑧)
5856, 57sseldd 3984 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛 ∈ 𝑧) β†’ 𝑛 ∈ 𝑍)
5958adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) β†’ 𝑛 ∈ 𝑍)
6019ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) β†’ (𝐴 ∩ (πΉβ€˜π‘›)) ∈ V)
6159, 60, 34syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) β†’ ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›) = (𝐴 ∩ (πΉβ€˜π‘›)))
6261fveq2d 6896 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) β†’ (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) = (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))))
6362sumeq2dv 15649 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ Σ𝑛 ∈ 𝑧 (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) = Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))))
6463oveq1d 7424 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ (Σ𝑛 ∈ 𝑧 (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) + π‘Œ) = (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
6554, 64breq12d 5162 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ ((π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) + π‘Œ) ↔ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
6665biimpd 228 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ ((π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) + π‘Œ) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
6766reximdva 3169 . . . . . . 7 (πœ‘ β†’ (βˆƒπ‘§ ∈ (𝒫 𝑍 ∩ Fin)(π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 ((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜((π‘˜ ∈ 𝑍 ↦ (𝐴 ∩ (πΉβ€˜π‘˜)))β€˜π‘›)) + π‘Œ) β†’ βˆƒπ‘§ ∈ (𝒫 𝑍 ∩ Fin)(π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
6853, 67mpd 15 . . . . . 6 (πœ‘ β†’ βˆƒπ‘§ ∈ (𝒫 𝑍 ∩ Fin)(π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
69 carageniuncllem2.m . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ β„€)
7069adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ 𝑀 ∈ β„€)
7155adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ 𝑧 βŠ† 𝑍)
72 elinel2 4197 . . . . . . . . . . 11 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) β†’ 𝑧 ∈ Fin)
7372adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ 𝑧 ∈ Fin)
7470, 12, 71, 73uzfissfz 44036 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 βŠ† (𝑀...π‘˜))
7574adantr 482 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ βˆƒπ‘˜ ∈ 𝑍 𝑧 βŠ† (𝑀...π‘˜))
7650ad3antrrr 729 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
77 fzfid 13938 . . . . . . . . . . . . . . . 16 (𝑧 βŠ† (𝑀...π‘˜) β†’ (𝑀...π‘˜) ∈ Fin)
78 id 22 . . . . . . . . . . . . . . . 16 (𝑧 βŠ† (𝑀...π‘˜) β†’ 𝑧 βŠ† (𝑀...π‘˜))
79 ssfi 9173 . . . . . . . . . . . . . . . 16 (((𝑀...π‘˜) ∈ Fin ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ 𝑧 ∈ Fin)
8077, 78, 79syl2anc 585 . . . . . . . . . . . . . . 15 (𝑧 βŠ† (𝑀...π‘˜) β†’ 𝑧 ∈ Fin)
8180adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ 𝑧 ∈ Fin)
821ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ 𝑧) β†’ 𝑂 ∈ OutMeas)
833ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ 𝑧) β†’ 𝐴 βŠ† 𝑋)
844ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ 𝑧) β†’ (π‘‚β€˜π΄) ∈ ℝ)
85 inss1 4229 . . . . . . . . . . . . . . . 16 (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝐴
8685a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ 𝑧) β†’ (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝐴)
8782, 2, 83, 84, 86omessre 45226 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ 𝑧) β†’ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
8881, 87fsumrecl 15680 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
8952rpred 13016 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘Œ ∈ ℝ)
9089adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ π‘Œ ∈ ℝ)
9188, 90readdcld 11243 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) ∈ ℝ)
9291ad4ant14 751 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) ∈ ℝ)
93 fzfid 13938 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑀...π‘˜) ∈ Fin)
9485a1i 11 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐴 ∩ (πΉβ€˜π‘›)) βŠ† 𝐴)
951, 2, 3, 4, 94omessre 45226 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
9695adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
9793, 96fsumrecl 15680 . . . . . . . . . . . . . 14 (πœ‘ β†’ Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
9897adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
9989adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ π‘Œ ∈ ℝ)
10098, 99readdcld 11243 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) β†’ (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) ∈ ℝ)
101100ad2antrr 725 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) ∈ ℝ)
102 simplr 768 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
10397adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
104 fzfid 13938 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (𝑀...π‘˜) ∈ Fin)
10596adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ ℝ)
106 0xr 11261 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
107106a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ 0 ∈ ℝ*)
108 pnfxr 11268 . . . . . . . . . . . . . . . . 17 +∞ ∈ ℝ*
109108a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ +∞ ∈ ℝ*)
1101, 2, 14omecl 45219 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ (0[,]+∞))
111110adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ (0[,]+∞))
112 iccgelb 13380 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ∈ (0[,]+∞)) β†’ 0 ≀ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))))
113107, 109, 111, 112syl3anc 1372 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ 0 ≀ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))))
114113adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) ∧ 𝑛 ∈ (𝑀...π‘˜)) β†’ 0 ≀ (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))))
115 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ 𝑧 βŠ† (𝑀...π‘˜))
116104, 105, 114, 115fsumless 15742 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) ≀ Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))))
11788, 103, 90, 116leadd1dd 11828 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) ≀ (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
118117ad4ant14 751 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) ≀ (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
11976, 92, 101, 102, 118ltletrd 11374 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) ∧ 𝑧 βŠ† (𝑀...π‘˜)) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
120119ex 414 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (𝑧 βŠ† (𝑀...π‘˜) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
121120reximdv 3171 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (βˆƒπ‘˜ ∈ 𝑍 𝑧 βŠ† (𝑀...π‘˜) β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
12275, 121mpd 15 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
123122rexlimdva2 3158 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘§ ∈ (𝒫 𝑍 ∩ Fin)(π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ 𝑧 (π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
12468, 123mpd 15 . . . . 5 (πœ‘ β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
12549ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝑍) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) = (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))))
126 simpr 486 . . . . . . . 8 (((πœ‘ ∧ π‘˜ ∈ 𝑍) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
127125, 126eqbrtrd 5171 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝑍) ∧ (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
128127ex 414 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
129128reximdva 3169 . . . . 5 (πœ‘ β†’ (βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜βˆͺ 𝑛 ∈ 𝑍 (𝐴 ∩ (πΉβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)))
130124, 129mpd 15 . . . 4 (πœ‘ β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
131 simpr 486 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝑍) ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ))
1321adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ 𝑂 ∈ OutMeas)
133 carageniuncllem2.s . . . . . . . . . 10 𝑆 = (CaraGenβ€˜π‘‚)
1343adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ 𝐴 βŠ† 𝑋)
1354adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘‚β€˜π΄) ∈ ℝ)
13639adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ 𝐸:π‘βŸΆπ‘†)
137 carageniuncllem2.g . . . . . . . . . 10 𝐺 = (𝑛 ∈ 𝑍 ↦ βˆͺ 𝑖 ∈ (𝑀...𝑛)(πΈβ€˜π‘–))
138 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ π‘˜ ∈ 𝑍)
139132, 133, 2, 134, 135, 12, 136, 137, 40, 138carageniuncllem1 45237 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) = (π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))))
140139oveq1d 7424 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) = ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ))
141140adantr 482 . . . . . . 7 (((πœ‘ ∧ π‘˜ ∈ 𝑍) ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) = ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ))
142131, 141breqtrd 5175 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ 𝑍) ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ))
143142ex 414 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)))
144143reximdva 3169 . . . 4 (πœ‘ β†’ (βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < (Σ𝑛 ∈ (𝑀...π‘˜)(π‘‚β€˜(𝐴 ∩ (πΉβ€˜π‘›))) + π‘Œ) β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)))
145130, 144mpd 15 . . 3 (πœ‘ β†’ βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ))
14673ad2ant1 1134 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ∈ ℝ)
14793ad2ant1 1134 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ∈ ℝ)
148 inss1 4229 . . . . . . . . . . 11 (𝐴 ∩ (πΊβ€˜π‘˜)) βŠ† 𝐴
149148a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (𝐴 ∩ (πΊβ€˜π‘˜)) βŠ† 𝐴)
150132, 2, 134, 135, 149omessre 45226 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) ∈ ℝ)
15189adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ π‘Œ ∈ ℝ)
152150, 151readdcld 11243 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) ∈ ℝ)
1531523adant3 1133 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) ∈ ℝ)
154 difssd 4133 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (𝐴 βˆ– (πΊβ€˜π‘˜)) βŠ† 𝐴)
155132, 2, 134, 135, 154omessre 45226 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜))) ∈ ℝ)
1561553adant3 1133 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜))) ∈ ℝ)
157 simp3 1139 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ))
158146, 153, 157ltled 11362 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ≀ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ))
159134ssdifssd 4143 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (𝐴 βˆ– (πΊβ€˜π‘˜)) βŠ† 𝑋)
160 oveq2 7417 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ (𝑀...𝑛) = (𝑀...π‘˜))
161160iuneq1d 5025 . . . . . . . . . . . . . 14 (𝑛 = π‘˜ β†’ βˆͺ 𝑖 ∈ (𝑀...𝑛)(πΈβ€˜π‘–) = βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–))
162 ovex 7442 . . . . . . . . . . . . . . 15 (𝑀...π‘˜) ∈ V
163 fvex 6905 . . . . . . . . . . . . . . 15 (πΈβ€˜π‘–) ∈ V
164162, 163iunex 7955 . . . . . . . . . . . . . 14 βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–) ∈ V
165161, 137, 164fvmpt 6999 . . . . . . . . . . . . 13 (π‘˜ ∈ 𝑍 β†’ (πΊβ€˜π‘˜) = βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–))
166 fveq2 6892 . . . . . . . . . . . . . . 15 (𝑖 = 𝑛 β†’ (πΈβ€˜π‘–) = (πΈβ€˜π‘›))
167166cbviunv 5044 . . . . . . . . . . . . . 14 βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–) = βˆͺ 𝑛 ∈ (𝑀...π‘˜)(πΈβ€˜π‘›)
168167a1i 11 . . . . . . . . . . . . 13 (π‘˜ ∈ 𝑍 β†’ βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–) = βˆͺ 𝑛 ∈ (𝑀...π‘˜)(πΈβ€˜π‘›))
169165, 168eqtrd 2773 . . . . . . . . . . . 12 (π‘˜ ∈ 𝑍 β†’ (πΊβ€˜π‘˜) = βˆͺ 𝑛 ∈ (𝑀...π‘˜)(πΈβ€˜π‘›))
170 elfzuz 13497 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...π‘˜) β†’ 𝑖 ∈ (β„€β‰₯β€˜π‘€))
17112eqcomi 2742 . . . . . . . . . . . . . . . . 17 (β„€β‰₯β€˜π‘€) = 𝑍
172171a1i 11 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀...π‘˜) β†’ (β„€β‰₯β€˜π‘€) = 𝑍)
173170, 172eleqtrd 2836 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀...π‘˜) β†’ 𝑖 ∈ 𝑍)
174173ssriv 3987 . . . . . . . . . . . . . 14 (𝑀...π‘˜) βŠ† 𝑍
175 iunss1 5012 . . . . . . . . . . . . . 14 ((𝑀...π‘˜) βŠ† 𝑍 β†’ βˆͺ 𝑛 ∈ (𝑀...π‘˜)(πΈβ€˜π‘›) βŠ† βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))
176174, 175ax-mp 5 . . . . . . . . . . . . 13 βˆͺ 𝑛 ∈ (𝑀...π‘˜)(πΈβ€˜π‘›) βŠ† βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)
177176a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ 𝑍 β†’ βˆͺ 𝑛 ∈ (𝑀...π‘˜)(πΈβ€˜π‘›) βŠ† βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))
178169, 177eqsstrd 4021 . . . . . . . . . . 11 (π‘˜ ∈ 𝑍 β†’ (πΊβ€˜π‘˜) βŠ† βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))
179178adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (πΊβ€˜π‘˜) βŠ† βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))
180179sscond 4142 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)) βŠ† (𝐴 βˆ– (πΊβ€˜π‘˜)))
181132, 2, 159, 180omessle 45214 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ≀ (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜))))
1821813adant3 1133 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) ≀ (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜))))
183146, 147, 153, 156, 158, 182le2addd 11833 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) ≀ (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))))
184150recnd 11242 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) ∈ β„‚)
18589recnd 11242 . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ β„‚)
186185adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ π‘Œ ∈ β„‚)
187155recnd 11242 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜))) ∈ β„‚)
188184, 186, 187add32d 11441 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) + π‘Œ))
189 rexadd 13211 . . . . . . . . . . . 12 (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) ∈ ℝ ∧ (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜))) ∈ ℝ) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) +𝑒 (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))))
190150, 155, 189syl2anc 585 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) +𝑒 (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))))
191190eqcomd 2739 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) +𝑒 (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))))
192 nfv 1918 . . . . . . . . . . . . . . 15 β„²π‘–πœ‘
19339adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (𝑀...π‘˜)) β†’ 𝐸:π‘βŸΆπ‘†)
194173adantl 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (𝑀...π‘˜)) β†’ 𝑖 ∈ 𝑍)
195193, 194ffvelcdmd 7088 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (𝑀...π‘˜)) β†’ (πΈβ€˜π‘–) ∈ 𝑆)
196192, 1, 133, 93, 195caragenfiiuncl 45231 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–) ∈ 𝑆)
197196adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–) ∈ 𝑆)
198137, 161, 138, 197fvmptd3 7022 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (πΊβ€˜π‘˜) = βˆͺ 𝑖 ∈ (𝑀...π‘˜)(πΈβ€˜π‘–))
199198, 197eqeltrd 2834 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (πΊβ€˜π‘˜) ∈ 𝑆)
200132, 133, 2, 199, 134caragensplit 45216 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) +𝑒 (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = (π‘‚β€˜π΄))
201191, 200eqtrd 2773 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = (π‘‚β€˜π΄))
202201oveq1d 7424 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) + π‘Œ) = ((π‘‚β€˜π΄) + π‘Œ))
203188, 202eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = ((π‘‚β€˜π΄) + π‘Œ))
2042033adant3 1133 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ (((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) + (π‘‚β€˜(𝐴 βˆ– (πΊβ€˜π‘˜)))) = ((π‘‚β€˜π΄) + π‘Œ))
205183, 204breqtrd 5175 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ 𝑍 ∧ (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ)) β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) ≀ ((π‘‚β€˜π΄) + π‘Œ))
2062053exp 1120 . . . 4 (πœ‘ β†’ (π‘˜ ∈ 𝑍 β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) ≀ ((π‘‚β€˜π΄) + π‘Œ))))
207206rexlimdv 3154 . . 3 (πœ‘ β†’ (βˆƒπ‘˜ ∈ 𝑍 (π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) < ((π‘‚β€˜(𝐴 ∩ (πΊβ€˜π‘˜))) + π‘Œ) β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) ≀ ((π‘‚β€˜π΄) + π‘Œ)))
208145, 207mpd 15 . 2 (πœ‘ β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) + (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) ≀ ((π‘‚β€˜π΄) + π‘Œ))
20911, 208eqbrtrd 5171 1 (πœ‘ β†’ ((π‘‚β€˜(𝐴 ∩ βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›))) +𝑒 (π‘‚β€˜(𝐴 βˆ– βˆͺ 𝑛 ∈ 𝑍 (πΈβ€˜π‘›)))) ≀ ((π‘‚β€˜π΄) + π‘Œ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  βˆͺ cuni 4909  βˆͺ ciun 4998  Disj wdisj 5114   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  Fincfn 8939  β„‚cc 11108  β„cr 11109  0cc0 11110   + caddc 11113  +∞cpnf 11245  β„*cxr 11247   < clt 11248   ≀ cle 11249  β„€cz 12558  β„€β‰₯cuz 12822  β„+crp 12974   +𝑒 cxad 13090  [,]cicc 13327  ...cfz 13484  ..^cfzo 13627  Ξ£csu 15632  OutMeascome 45205  CaraGenccaragen 45207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-ac2 10458  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-oadd 8470  df-omul 8471  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-oi 9505  df-card 9934  df-acn 9937  df-ac 10111  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-xadd 13093  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633  df-sumge0 45079  df-ome 45206  df-caragen 45208
This theorem is referenced by:  carageniuncl  45239
  Copyright terms: Public domain W3C validator