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

Theorem meaiininclem 45287
Description: Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
meaiininclem.m (𝜑𝑀 ∈ Meas)
meaiininclem.n (𝜑𝑁 ∈ ℤ)
meaiininclem.z 𝑍 = (ℤ𝑁)
meaiininclem.e (𝜑𝐸:𝑍⟶dom 𝑀)
meaiininclem.i ((𝜑𝑛𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛))
meaiininclem.k (𝜑𝐾 ∈ (ℤ𝑁))
meaiininclem.r (𝜑 → (𝑀‘(𝐸𝐾)) ∈ ℝ)
meaiininclem.s 𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
meaiininclem.g 𝐺 = (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛)))
meaiininclem.f 𝐹 = 𝑛𝑍 (𝐺𝑛)
Assertion
Ref Expression
meaiininclem (𝜑𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)))
Distinct variable groups:   𝑛,𝐸   𝑛,𝐹   𝑛,𝐺   𝑛,𝐾   𝑛,𝑀   𝑛,𝑁   𝑛,𝑍   𝜑,𝑛
Allowed substitution hint:   𝑆(𝑛)

Proof of Theorem meaiininclem
Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 meaiininclem.k . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (ℤ𝑁))
2 uzss 12847 . . . . . . . . . . . . . 14 (𝐾 ∈ (ℤ𝑁) → (ℤ𝐾) ⊆ (ℤ𝑁))
31, 2syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℤ𝐾) ⊆ (ℤ𝑁))
4 meaiininclem.z . . . . . . . . . . . . 13 𝑍 = (ℤ𝑁)
53, 4sseqtrrdi 4033 . . . . . . . . . . . 12 (𝜑 → (ℤ𝐾) ⊆ 𝑍)
65adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝐾)) → (ℤ𝐾) ⊆ 𝑍)
7 simpr 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝐾)) → 𝑛 ∈ (ℤ𝐾))
86, 7sseldd 3983 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝐾)) → 𝑛𝑍)
9 meaiininclem.g . . . . . . . . . . . 12 𝐺 = (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛)))
109a1i 11 . . . . . . . . . . 11 (𝜑𝐺 = (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛))))
11 meaiininclem.m . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ Meas)
12 eqid 2732 . . . . . . . . . . . . . . 15 dom 𝑀 = dom 𝑀
1311, 12dmmeasal 45253 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑀 ∈ SAlg)
1413adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → dom 𝑀 ∈ SAlg)
151, 4eleqtrrdi 2844 . . . . . . . . . . . . . . 15 (𝜑𝐾𝑍)
16 meaiininclem.e . . . . . . . . . . . . . . . 16 (𝜑𝐸:𝑍⟶dom 𝑀)
1716ffvelcdmda 7086 . . . . . . . . . . . . . . 15 ((𝜑𝐾𝑍) → (𝐸𝐾) ∈ dom 𝑀)
1815, 17mpdan 685 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝐾) ∈ dom 𝑀)
1918adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝐸𝐾) ∈ dom 𝑀)
2016ffvelcdmda 7086 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ dom 𝑀)
21 saldifcl2 45129 . . . . . . . . . . . . 13 ((dom 𝑀 ∈ SAlg ∧ (𝐸𝐾) ∈ dom 𝑀 ∧ (𝐸𝑛) ∈ dom 𝑀) → ((𝐸𝐾) ∖ (𝐸𝑛)) ∈ dom 𝑀)
2214, 19, 20, 21syl3anc 1371 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ∈ dom 𝑀)
2322elexd 3494 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ∈ V)
2410, 23fvmpt2d 7011 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝐺𝑛) = ((𝐸𝐾) ∖ (𝐸𝑛)))
258, 24syldan 591 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐺𝑛) = ((𝐸𝐾) ∖ (𝐸𝑛)))
2625fveq2d 6895 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) = (𝑀‘((𝐸𝐾) ∖ (𝐸𝑛))))
2711adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → 𝑀 ∈ Meas)
2818adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐸𝐾) ∈ dom 𝑀)
29 meaiininclem.r . . . . . . . . . 10 (𝜑 → (𝑀‘(𝐸𝐾)) ∈ ℝ)
3029adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝐾)) ∈ ℝ)
318, 20syldan 591 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐸𝑛) ∈ dom 𝑀)
32 simpl 483 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → 𝜑)
3332, 5syl 17 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → (ℤ𝐾) ⊆ 𝑍)
34 elfzouz 13638 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ𝐾))
3534adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ𝐾))
3633, 35sseldd 3983 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → 𝑚𝑍)
37 eleq1w 2816 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝑛𝑍𝑚𝑍))
3837anbi2d 629 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((𝜑𝑛𝑍) ↔ (𝜑𝑚𝑍)))
39 fvoveq1 7434 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40 fveq2 6891 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐸𝑛) = (𝐸𝑚))
4139, 40sseq12d 4015 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛) ↔ (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚)))
4238, 41imbi12d 344 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (((𝜑𝑛𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛)) ↔ ((𝜑𝑚𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))))
43 meaiininclem.i . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛))
4442, 43chvarvv 2002 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))
4532, 36, 44syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))
4645adantlr 713 . . . . . . . . . 10 (((𝜑𝑛 ∈ (ℤ𝐾)) ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))
477, 46ssdec 43865 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐸𝑛) ⊆ (𝐸𝐾))
4827, 28, 30, 31, 47meadif 45280 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘((𝐸𝐾) ∖ (𝐸𝑛))) = ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛))))
4926, 48eqtrd 2772 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) = ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛))))
5049oveq2d 7427 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛))) = ((𝑀‘(𝐸𝐾)) − ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛)))))
5129recnd 11244 . . . . . . . 8 (𝜑 → (𝑀‘(𝐸𝐾)) ∈ ℂ)
5251adantr 481 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝐾)) ∈ ℂ)
5327, 28, 30, 47, 31meassre 45278 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝑛)) ∈ ℝ)
5453recnd 11244 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝑛)) ∈ ℂ)
5552, 54nncand 11578 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑀‘(𝐸𝐾)) − ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛)))) = (𝑀‘(𝐸𝑛)))
5650, 55eqtr2d 2773 . . . . 5 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝑛)) = ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛))))
5756mpteq2dva 5248 . . . 4 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) = (𝑛 ∈ (ℤ𝐾) ↦ ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛)))))
58 nfv 1917 . . . . 5 𝑛𝜑
59 eqid 2732 . . . . 5 (ℤ𝐾) = (ℤ𝐾)
601eluzelzd 44170 . . . . 5 (𝜑𝐾 ∈ ℤ)
61 difssd 4132 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ⊆ (𝐸𝐾))
6224, 61eqsstrd 4020 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐺𝑛) ⊆ (𝐸𝐾))
638, 62syldan 591 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐺𝑛) ⊆ (𝐸𝐾))
6422, 9fmptd 7115 . . . . . . . . 9 (𝜑𝐺:𝑍⟶dom 𝑀)
6564ffvelcdmda 7086 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ dom 𝑀)
668, 65syldan 591 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐺𝑛) ∈ dom 𝑀)
6727, 28, 30, 63, 66meassre 45278 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) ∈ ℝ)
6867recnd 11244 . . . . 5 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) ∈ ℂ)
69 meaiininclem.n . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
7043sscond 4141 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ⊆ ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
7140difeq2d 4122 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → ((𝐸𝐾) ∖ (𝐸𝑛)) = ((𝐸𝐾) ∖ (𝐸𝑚)))
7271cbvmptv 5261 . . . . . . . . . . . 12 (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛))) = (𝑚𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑚)))
739, 72eqtri 2760 . . . . . . . . . . 11 𝐺 = (𝑚𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑚)))
74 fveq2 6891 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝐸𝑚) = (𝐸‘(𝑛 + 1)))
7574difeq2d 4122 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((𝐸𝐾) ∖ (𝐸𝑚)) = ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
764peano2uzs 12888 . . . . . . . . . . . 12 (𝑛𝑍 → (𝑛 + 1) ∈ 𝑍)
7776adantl 482 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → (𝑛 + 1) ∈ 𝑍)
78 fvex 6904 . . . . . . . . . . . . 13 (𝐸𝐾) ∈ V
7978difexi 5328 . . . . . . . . . . . 12 ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
8079a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
8173, 75, 77, 80fvmptd3 7021 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
8224, 81sseq12d 4015 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐺𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸𝐾) ∖ (𝐸𝑛)) ⊆ ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1)))))
8370, 82mpbird 256 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐺𝑛) ⊆ (𝐺‘(𝑛 + 1)))
8411adantr 481 . . . . . . . . 9 ((𝜑𝑛𝑍) → 𝑀 ∈ Meas)
8584, 12, 65, 19, 62meassle 45264 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝑀‘(𝐺𝑛)) ≤ (𝑀‘(𝐸𝐾)))
86 eqid 2732 . . . . . . . 8 (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛))) = (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛)))
8711, 69, 4, 64, 83, 29, 85, 86meaiuninc2 45283 . . . . . . 7 (𝜑 → (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛)))
88 eqid 2732 . . . . . . . 8 (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) = (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛)))
894, 86, 15, 88climresmpt 44460 . . . . . . 7 (𝜑 → ((𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛)) ↔ (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛))))
9087, 89mpbird 256 . . . . . 6 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛)))
91 meaiininclem.f . . . . . . . . 9 𝐹 = 𝑛𝑍 (𝐺𝑛)
9291eqcomi 2741 . . . . . . . 8 𝑛𝑍 (𝐺𝑛) = 𝐹
9392fveq2i 6894 . . . . . . 7 (𝑀 𝑛𝑍 (𝐺𝑛)) = (𝑀𝐹)
9493a1i 11 . . . . . 6 (𝜑 → (𝑀 𝑛𝑍 (𝐺𝑛)) = (𝑀𝐹))
9590, 94breqtrd 5174 . . . . 5 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀𝐹))
9658, 59, 60, 51, 68, 95climsubc1mpt 44463 . . . 4 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛)))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
9757, 96eqbrtrd 5170 . . 3 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
98 eqid 2732 . . . 4 (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
99 eqid 2732 . . . 4 (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) = (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛)))
1004, 98, 15, 99climresmpt 44460 . . 3 (𝜑 → ((𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)) ↔ (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹))))
10197, 100mpbid 231 . 2 (𝜑 → (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
102 meaiininclem.s . . . 4 𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
103102a1i 11 . . 3 (𝜑𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))))
104 eqidd 2733 . . . . . 6 (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))))
1054uzct 43838 . . . . . . . . . 10 𝑍 ≼ ω
106105a1i 11 . . . . . . . . 9 (𝜑𝑍 ≼ ω)
10713, 106, 65saliuncl 45124 . . . . . . . 8 (𝜑 𝑛𝑍 (𝐺𝑛) ∈ dom 𝑀)
10891, 107eqeltrid 2837 . . . . . . 7 (𝜑𝐹 ∈ dom 𝑀)
109 saldifcl2 45129 . . . . . . . 8 ((dom 𝑀 ∈ SAlg ∧ (𝐸𝐾) ∈ dom 𝑀𝐹 ∈ dom 𝑀) → ((𝐸𝐾) ∖ 𝐹) ∈ dom 𝑀)
11013, 18, 108, 109syl3anc 1371 . . . . . . 7 (𝜑 → ((𝐸𝐾) ∖ 𝐹) ∈ dom 𝑀)
111 disjdif 4471 . . . . . . . 8 (𝐹 ∩ ((𝐸𝐾) ∖ 𝐹)) = ∅
112111a1i 11 . . . . . . 7 (𝜑 → (𝐹 ∩ ((𝐸𝐾) ∖ 𝐹)) = ∅)
11362iunssd 5053 . . . . . . . . 9 (𝜑 𝑛𝑍 (𝐺𝑛) ⊆ (𝐸𝐾))
11491, 113eqsstrid 4030 . . . . . . . 8 (𝜑𝐹 ⊆ (𝐸𝐾))
11511, 18, 29, 114, 108meassre 45278 . . . . . . 7 (𝜑 → (𝑀𝐹) ∈ ℝ)
116 difssd 4132 . . . . . . . 8 (𝜑 → ((𝐸𝐾) ∖ 𝐹) ⊆ (𝐸𝐾))
11711, 18, 29, 116, 110meassre 45278 . . . . . . 7 (𝜑 → (𝑀‘((𝐸𝐾) ∖ 𝐹)) ∈ ℝ)
11811, 12, 108, 110, 112, 115, 117meadjunre 45277 . . . . . 6 (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))) = ((𝑀𝐹) + (𝑀‘((𝐸𝐾) ∖ 𝐹))))
119 undif 4481 . . . . . . . 8 (𝐹 ⊆ (𝐸𝐾) ↔ (𝐹 ∪ ((𝐸𝐾) ∖ 𝐹)) = (𝐸𝐾))
120114, 119sylib 217 . . . . . . 7 (𝜑 → (𝐹 ∪ ((𝐸𝐾) ∖ 𝐹)) = (𝐸𝐾))
121120fveq2d 6895 . . . . . 6 (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐸𝐾)))
122104, 118, 1213eqtr3d 2780 . . . . 5 (𝜑 → ((𝑀𝐹) + (𝑀‘((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐸𝐾)))
123115recnd 11244 . . . . . 6 (𝜑 → (𝑀𝐹) ∈ ℂ)
124117recnd 11244 . . . . . 6 (𝜑 → (𝑀‘((𝐸𝐾) ∖ 𝐹)) ∈ ℂ)
12551, 123, 124subaddd 11591 . . . . 5 (𝜑 → (((𝑀‘(𝐸𝐾)) − (𝑀𝐹)) = (𝑀‘((𝐸𝐾) ∖ 𝐹)) ↔ ((𝑀𝐹) + (𝑀‘((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐸𝐾))))
126122, 125mpbird 256 . . . 4 (𝜑 → ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)) = (𝑀‘((𝐸𝐾) ∖ 𝐹)))
127 simpllr 774 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
128 simplr 767 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑛𝑍)
129 eldifi 4126 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸𝐾))
130129ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 ∈ (𝐸𝐾))
131 simpr 485 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → ¬ 𝑥 ∈ (𝐸𝑛))
132130, 131eldifd 3959 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
133 rspe 3246 . . . . . . . . . . . . . . 15 ((𝑛𝑍𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛))) → ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
134128, 132, 133syl2anc 584 . . . . . . . . . . . . . 14 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
135 eliun 5001 . . . . . . . . . . . . . 14 (𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)) ↔ ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
136134, 135sylibr 233 . . . . . . . . . . . . 13 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
137136adantlll 716 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
13891a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝐹 = 𝑛𝑍 (𝐺𝑛))
13924iuneq2dv 5021 . . . . . . . . . . . . . . 15 (𝜑 𝑛𝑍 (𝐺𝑛) = 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
140138, 139eqtrd 2772 . . . . . . . . . . . . . 14 (𝜑𝐹 = 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
141140eqcomd 2738 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)) = 𝐹)
142141ad3antrrr 728 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)) = 𝐹)
143137, 142eleqtrd 2835 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥𝐹)
144 elndif 4128 . . . . . . . . . . 11 (𝑥𝐹 → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
145143, 144syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
146127, 145condan 816 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) → 𝑥 ∈ (𝐸𝑛))
147146ralrimiva 3146 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) → ∀𝑛𝑍 𝑥 ∈ (𝐸𝑛))
148 vex 3478 . . . . . . . . 9 𝑥 ∈ V
149 eliin 5002 . . . . . . . . 9 (𝑥 ∈ V → (𝑥 𝑛𝑍 (𝐸𝑛) ↔ ∀𝑛𝑍 𝑥 ∈ (𝐸𝑛)))
150148, 149ax-mp 5 . . . . . . . 8 (𝑥 𝑛𝑍 (𝐸𝑛) ↔ ∀𝑛𝑍 𝑥 ∈ (𝐸𝑛))
151147, 150sylibr 233 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) → 𝑥 𝑛𝑍 (𝐸𝑛))
152151ssd 43857 . . . . . 6 (𝜑 → ((𝐸𝐾) ∖ 𝐹) ⊆ 𝑛𝑍 (𝐸𝑛))
153 ssid 4004 . . . . . . . . . . . 12 (𝐸𝐾) ⊆ (𝐸𝐾)
154153a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸𝐾) ⊆ (𝐸𝐾))
155 fveq2 6891 . . . . . . . . . . . . 13 (𝑛 = 𝐾 → (𝐸𝑛) = (𝐸𝐾))
156155sseq1d 4013 . . . . . . . . . . . 12 (𝑛 = 𝐾 → ((𝐸𝑛) ⊆ (𝐸𝐾) ↔ (𝐸𝐾) ⊆ (𝐸𝐾)))
157156rspcev 3612 . . . . . . . . . . 11 ((𝐾𝑍 ∧ (𝐸𝐾) ⊆ (𝐸𝐾)) → ∃𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
15815, 154, 157syl2anc 584 . . . . . . . . . 10 (𝜑 → ∃𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
159 iinss 5059 . . . . . . . . . 10 (∃𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾) → 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
160158, 159syl 17 . . . . . . . . 9 (𝜑 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
161160adantr 481 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
162 simpr 485 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑥 𝑛𝑍 (𝐸𝑛))
163161, 162sseldd 3983 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑥 ∈ (𝐸𝐾))
164 nfcv 2903 . . . . . . . . . . . . 13 𝑛𝑥
165 nfii1 5032 . . . . . . . . . . . . 13 𝑛 𝑛𝑍 (𝐸𝑛)
166164, 165nfel 2917 . . . . . . . . . . . 12 𝑛 𝑥 𝑛𝑍 (𝐸𝑛)
167 iinss2 5060 . . . . . . . . . . . . . . . 16 (𝑛𝑍 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝑛))
168167adantl 482 . . . . . . . . . . . . . . 15 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝑛))
169 simpl 483 . . . . . . . . . . . . . . 15 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → 𝑥 𝑛𝑍 (𝐸𝑛))
170168, 169sseldd 3983 . . . . . . . . . . . . . 14 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → 𝑥 ∈ (𝐸𝑛))
171 elndif 4128 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐸𝑛) → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
172170, 171syl 17 . . . . . . . . . . . . 13 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
173172ex 413 . . . . . . . . . . . 12 (𝑥 𝑛𝑍 (𝐸𝑛) → (𝑛𝑍 → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛))))
174166, 173ralrimi 3254 . . . . . . . . . . 11 (𝑥 𝑛𝑍 (𝐸𝑛) → ∀𝑛𝑍 ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
175 ralnex 3072 . . . . . . . . . . 11 (∀𝑛𝑍 ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)) ↔ ¬ ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
176174, 175sylib 217 . . . . . . . . . 10 (𝑥 𝑛𝑍 (𝐸𝑛) → ¬ ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
177176, 135sylnibr 328 . . . . . . . . 9 (𝑥 𝑛𝑍 (𝐸𝑛) → ¬ 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
178177adantl 482 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → ¬ 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
179140adantr 481 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝐹 = 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
180178, 179neleqtrrd 2856 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → ¬ 𝑥𝐹)
181163, 180eldifd 3959 . . . . . 6 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
182152, 181eqelssd 4003 . . . . 5 (𝜑 → ((𝐸𝐾) ∖ 𝐹) = 𝑛𝑍 (𝐸𝑛))
183182fveq2d 6895 . . . 4 (𝜑 → (𝑀‘((𝐸𝐾) ∖ 𝐹)) = (𝑀 𝑛𝑍 (𝐸𝑛)))
184126, 183eqtr2d 2773 . . 3 (𝜑 → (𝑀 𝑛𝑍 (𝐸𝑛)) = ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
185103, 184breq12d 5161 . 2 (𝜑 → (𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)) ↔ (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹))))
186101, 185mpbird 256 1 (𝜑𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  wrex 3070  Vcvv 3474  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322   ciun 4997   ciin 4998   class class class wbr 5148  cmpt 5231  dom cdm 5676  wf 6539  cfv 6543  (class class class)co 7411  ωcom 7857  cdom 8939  cc 11110  cr 11111  1c1 11113   + caddc 11115  cmin 11446  cz 12560  cuz 12824  ..^cfzo 13629  cli 15430  SAlgcsalg 45109  Meascmea 45250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-omul 8473  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-acn 9939  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-xadd 13095  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-sum 15635  df-salg 45110  df-sumge0 45164  df-mea 45251
This theorem is referenced by:  meaiininc  45288
  Copyright terms: Public domain W3C validator