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 41343
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 11910 . . . . . . . . . . . . . 14 (𝐾 ∈ (ℤ𝑁) → (ℤ𝐾) ⊆ (ℤ𝑁))
31, 2syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℤ𝐾) ⊆ (ℤ𝑁))
4 meaiininclem.z . . . . . . . . . . . . 13 𝑍 = (ℤ𝑁)
53, 4syl6sseqr 3814 . . . . . . . . . . . 12 (𝜑 → (ℤ𝐾) ⊆ 𝑍)
65adantr 472 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝐾)) → (ℤ𝐾) ⊆ 𝑍)
7 simpr 477 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝐾)) → 𝑛 ∈ (ℤ𝐾))
86, 7sseldd 3764 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝐾)) → 𝑛𝑍)
9 meaiininclem.g . . . . . . . . . . . 12 𝐺 = (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛)))
109a1i 11 . . . . . . . . . . 11 (𝜑𝐺 = (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛))))
11 meaiininclem.m . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ Meas)
12 eqid 2765 . . . . . . . . . . . . . . 15 dom 𝑀 = dom 𝑀
1311, 12dmmeasal 41309 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑀 ∈ SAlg)
1413adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → dom 𝑀 ∈ SAlg)
151, 4syl6eleqr 2855 . . . . . . . . . . . . . . 15 (𝜑𝐾𝑍)
16 meaiininclem.e . . . . . . . . . . . . . . . 16 (𝜑𝐸:𝑍⟶dom 𝑀)
1716ffvelrnda 6551 . . . . . . . . . . . . . . 15 ((𝜑𝐾𝑍) → (𝐸𝐾) ∈ dom 𝑀)
1815, 17mpdan 678 . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝐾) ∈ dom 𝑀)
1918adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝐸𝐾) ∈ dom 𝑀)
2016ffvelrnda 6551 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ dom 𝑀)
21 saldifcl2 41186 . . . . . . . . . . . . 13 ((dom 𝑀 ∈ SAlg ∧ (𝐸𝐾) ∈ dom 𝑀 ∧ (𝐸𝑛) ∈ dom 𝑀) → ((𝐸𝐾) ∖ (𝐸𝑛)) ∈ dom 𝑀)
2214, 19, 20, 21syl3anc 1490 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ∈ dom 𝑀)
2322elexd 3367 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ∈ V)
2410, 23fvmpt2d 6484 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝐺𝑛) = ((𝐸𝐾) ∖ (𝐸𝑛)))
258, 24syldan 585 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐺𝑛) = ((𝐸𝐾) ∖ (𝐸𝑛)))
2625fveq2d 6381 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) = (𝑀‘((𝐸𝐾) ∖ (𝐸𝑛))))
2711adantr 472 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → 𝑀 ∈ Meas)
2818adantr 472 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐸𝐾) ∈ dom 𝑀)
29 meaiininclem.r . . . . . . . . . 10 (𝜑 → (𝑀‘(𝐸𝐾)) ∈ ℝ)
3029adantr 472 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝐾)) ∈ ℝ)
318, 20syldan 585 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐸𝑛) ∈ dom 𝑀)
32 simpl 474 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → 𝜑)
3332, 5syl 17 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → (ℤ𝐾) ⊆ 𝑍)
34 elfzouz 12685 . . . . . . . . . . . . . 14 (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ𝐾))
3534adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ𝐾))
3633, 35sseldd 3764 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → 𝑚𝑍)
37 eleq1w 2827 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝑛𝑍𝑚𝑍))
3837anbi2d 622 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((𝜑𝑛𝑍) ↔ (𝜑𝑚𝑍)))
39 fvoveq1 6867 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40 fveq2 6377 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → (𝐸𝑛) = (𝐸𝑚))
4139, 40sseq12d 3796 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛) ↔ (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚)))
4238, 41imbi12d 335 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (((𝜑𝑛𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛)) ↔ ((𝜑𝑚𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))))
43 meaiininclem.i . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸𝑛))
4442, 43chvarv 2369 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))
4532, 36, 44syl2anc 579 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))
4645adantlr 706 . . . . . . . . . 10 (((𝜑𝑛 ∈ (ℤ𝐾)) ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸𝑚))
477, 46ssdec 39919 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐸𝑛) ⊆ (𝐸𝐾))
4827, 28, 30, 31, 47meadif 41336 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘((𝐸𝐾) ∖ (𝐸𝑛))) = ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛))))
4926, 48eqtrd 2799 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) = ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛))))
5049oveq2d 6860 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛))) = ((𝑀‘(𝐸𝐾)) − ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛)))))
5129recnd 10324 . . . . . . . 8 (𝜑 → (𝑀‘(𝐸𝐾)) ∈ ℂ)
5251adantr 472 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝐾)) ∈ ℂ)
5327, 28, 30, 47, 31meassre 41334 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝑛)) ∈ ℝ)
5453recnd 10324 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝑛)) ∈ ℂ)
5552, 54nncand 10653 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → ((𝑀‘(𝐸𝐾)) − ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐸𝑛)))) = (𝑀‘(𝐸𝑛)))
5650, 55eqtr2d 2800 . . . . 5 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐸𝑛)) = ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛))))
5756mpteq2dva 4905 . . . 4 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) = (𝑛 ∈ (ℤ𝐾) ↦ ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛)))))
58 nfv 2009 . . . . 5 𝑛𝜑
59 eqid 2765 . . . . 5 (ℤ𝐾) = (ℤ𝐾)
601eluzelzd 40232 . . . . 5 (𝜑𝐾 ∈ ℤ)
61 difssd 3902 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ⊆ (𝐸𝐾))
6224, 61eqsstrd 3801 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐺𝑛) ⊆ (𝐸𝐾))
638, 62syldan 585 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐺𝑛) ⊆ (𝐸𝐾))
6422, 9fmptd 6576 . . . . . . . . 9 (𝜑𝐺:𝑍⟶dom 𝑀)
6564ffvelrnda 6551 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐺𝑛) ∈ dom 𝑀)
668, 65syldan 585 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝐺𝑛) ∈ dom 𝑀)
6727, 28, 30, 63, 66meassre 41334 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) ∈ ℝ)
6867recnd 10324 . . . . 5 ((𝜑𝑛 ∈ (ℤ𝐾)) → (𝑀‘(𝐺𝑛)) ∈ ℂ)
69 meaiininclem.n . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
7043sscond 3911 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸𝑛)) ⊆ ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
7140difeq2d 3892 . . . . . . . . . . . . . 14 (𝑛 = 𝑚 → ((𝐸𝐾) ∖ (𝐸𝑛)) = ((𝐸𝐾) ∖ (𝐸𝑚)))
7271cbvmptv 4911 . . . . . . . . . . . . 13 (𝑛𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑛))) = (𝑚𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑚)))
739, 72eqtri 2787 . . . . . . . . . . . 12 𝐺 = (𝑚𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑚)))
7473a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝐺 = (𝑚𝑍 ↦ ((𝐸𝐾) ∖ (𝐸𝑚))))
75 fveq2 6377 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (𝐸𝑚) = (𝐸‘(𝑛 + 1)))
7675difeq2d 3892 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → ((𝐸𝐾) ∖ (𝐸𝑚)) = ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
7776adantl 473 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑚 = (𝑛 + 1)) → ((𝐸𝐾) ∖ (𝐸𝑚)) = ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
784peano2uzs 11945 . . . . . . . . . . . 12 (𝑛𝑍 → (𝑛 + 1) ∈ 𝑍)
7978adantl 473 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → (𝑛 + 1) ∈ 𝑍)
80 fvex 6390 . . . . . . . . . . . . 13 (𝐸𝐾) ∈ V
8180difexi 4972 . . . . . . . . . . . 12 ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
8281a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
8374, 77, 79, 82fvmptd 6479 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1))))
8424, 83sseq12d 3796 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐺𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸𝐾) ∖ (𝐸𝑛)) ⊆ ((𝐸𝐾) ∖ (𝐸‘(𝑛 + 1)))))
8570, 84mpbird 248 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐺𝑛) ⊆ (𝐺‘(𝑛 + 1)))
8611adantr 472 . . . . . . . . 9 ((𝜑𝑛𝑍) → 𝑀 ∈ Meas)
8786, 12, 65, 19, 62meassle 41320 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝑀‘(𝐺𝑛)) ≤ (𝑀‘(𝐸𝐾)))
88 eqid 2765 . . . . . . . 8 (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛))) = (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛)))
8911, 69, 4, 64, 85, 29, 87, 88meaiuninc2 41339 . . . . . . 7 (𝜑 → (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛)))
90 eqid 2765 . . . . . . . 8 (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) = (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛)))
914, 88, 15, 90climresmpt 40532 . . . . . . 7 (𝜑 → ((𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛)) ↔ (𝑛𝑍 ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛))))
9289, 91mpbird 248 . . . . . 6 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀 𝑛𝑍 (𝐺𝑛)))
93 meaiininclem.f . . . . . . . . 9 𝐹 = 𝑛𝑍 (𝐺𝑛)
9493eqcomi 2774 . . . . . . . 8 𝑛𝑍 (𝐺𝑛) = 𝐹
9594fveq2i 6380 . . . . . . 7 (𝑀 𝑛𝑍 (𝐺𝑛)) = (𝑀𝐹)
9695a1i 11 . . . . . 6 (𝜑 → (𝑀 𝑛𝑍 (𝐺𝑛)) = (𝑀𝐹))
9792, 96breqtrd 4837 . . . . 5 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐺𝑛))) ⇝ (𝑀𝐹))
9858, 59, 60, 51, 68, 97climsubc1mpt 40535 . . . 4 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ ((𝑀‘(𝐸𝐾)) − (𝑀‘(𝐺𝑛)))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
9957, 98eqbrtrd 4833 . . 3 (𝜑 → (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
100 eqid 2765 . . . 4 (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
101 eqid 2765 . . . 4 (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) = (𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛)))
1024, 100, 15, 101climresmpt 40532 . . 3 (𝜑 → ((𝑛 ∈ (ℤ𝐾) ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)) ↔ (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹))))
10399, 102mpbid 223 . 2 (𝜑 → (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
104 meaiininclem.s . . . 4 𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
105104a1i 11 . . 3 (𝜑𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))))
106 eqidd 2766 . . . . . 6 (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))))
1074uzct 39886 . . . . . . . . . 10 𝑍 ≼ ω
108107a1i 11 . . . . . . . . 9 (𝜑𝑍 ≼ ω)
10913, 108, 65saliuncl 41182 . . . . . . . 8 (𝜑 𝑛𝑍 (𝐺𝑛) ∈ dom 𝑀)
11093, 109syl5eqel 2848 . . . . . . 7 (𝜑𝐹 ∈ dom 𝑀)
111 saldifcl2 41186 . . . . . . . 8 ((dom 𝑀 ∈ SAlg ∧ (𝐸𝐾) ∈ dom 𝑀𝐹 ∈ dom 𝑀) → ((𝐸𝐾) ∖ 𝐹) ∈ dom 𝑀)
11213, 18, 110, 111syl3anc 1490 . . . . . . 7 (𝜑 → ((𝐸𝐾) ∖ 𝐹) ∈ dom 𝑀)
113 disjdif 4202 . . . . . . . 8 (𝐹 ∩ ((𝐸𝐾) ∖ 𝐹)) = ∅
114113a1i 11 . . . . . . 7 (𝜑 → (𝐹 ∩ ((𝐸𝐾) ∖ 𝐹)) = ∅)
11562iunssd 39925 . . . . . . . . 9 (𝜑 𝑛𝑍 (𝐺𝑛) ⊆ (𝐸𝐾))
11693, 115syl5eqss 3811 . . . . . . . 8 (𝜑𝐹 ⊆ (𝐸𝐾))
11711, 18, 29, 116, 110meassre 41334 . . . . . . 7 (𝜑 → (𝑀𝐹) ∈ ℝ)
118 difssd 3902 . . . . . . . 8 (𝜑 → ((𝐸𝐾) ∖ 𝐹) ⊆ (𝐸𝐾))
11911, 18, 29, 118, 112meassre 41334 . . . . . . 7 (𝜑 → (𝑀‘((𝐸𝐾) ∖ 𝐹)) ∈ ℝ)
12011, 12, 110, 112, 114, 117, 119meadjunre 41333 . . . . . 6 (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))) = ((𝑀𝐹) + (𝑀‘((𝐸𝐾) ∖ 𝐹))))
121 undif 4211 . . . . . . . 8 (𝐹 ⊆ (𝐸𝐾) ↔ (𝐹 ∪ ((𝐸𝐾) ∖ 𝐹)) = (𝐸𝐾))
122116, 121sylib 209 . . . . . . 7 (𝜑 → (𝐹 ∪ ((𝐸𝐾) ∖ 𝐹)) = (𝐸𝐾))
123122fveq2d 6381 . . . . . 6 (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐸𝐾)))
124106, 120, 1233eqtr3d 2807 . . . . 5 (𝜑 → ((𝑀𝐹) + (𝑀‘((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐸𝐾)))
125117recnd 10324 . . . . . 6 (𝜑 → (𝑀𝐹) ∈ ℂ)
126119recnd 10324 . . . . . 6 (𝜑 → (𝑀‘((𝐸𝐾) ∖ 𝐹)) ∈ ℂ)
12751, 125, 126subaddd 10666 . . . . 5 (𝜑 → (((𝑀‘(𝐸𝐾)) − (𝑀𝐹)) = (𝑀‘((𝐸𝐾) ∖ 𝐹)) ↔ ((𝑀𝐹) + (𝑀‘((𝐸𝐾) ∖ 𝐹))) = (𝑀‘(𝐸𝐾))))
128124, 127mpbird 248 . . . 4 (𝜑 → ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)) = (𝑀‘((𝐸𝐾) ∖ 𝐹)))
129 simpllr 793 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
130 simplr 785 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑛𝑍)
131 eldifi 3896 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸𝐾))
132131ad2antrr 717 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 ∈ (𝐸𝐾))
133 simpr 477 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → ¬ 𝑥 ∈ (𝐸𝑛))
134132, 133eldifd 3745 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
135 rspe 3149 . . . . . . . . . . . . . . 15 ((𝑛𝑍𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛))) → ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
136130, 134, 135syl2anc 579 . . . . . . . . . . . . . 14 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
137 eliun 4682 . . . . . . . . . . . . . 14 (𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)) ↔ ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
138136, 137sylibr 225 . . . . . . . . . . . . 13 (((𝑥 ∈ ((𝐸𝐾) ∖ 𝐹) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
139138adantlll 709 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
14093a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝐹 = 𝑛𝑍 (𝐺𝑛))
14124iuneq2dv 4700 . . . . . . . . . . . . . . 15 (𝜑 𝑛𝑍 (𝐺𝑛) = 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
142140, 141eqtrd 2799 . . . . . . . . . . . . . 14 (𝜑𝐹 = 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
143142eqcomd 2771 . . . . . . . . . . . . 13 (𝜑 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)) = 𝐹)
144143ad3antrrr 721 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)) = 𝐹)
145139, 144eleqtrd 2846 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → 𝑥𝐹)
146 elndif 3898 . . . . . . . . . . 11 (𝑥𝐹 → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
147145, 146syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) ∧ ¬ 𝑥 ∈ (𝐸𝑛)) → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
148129, 147condan 852 . . . . . . . . 9 (((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) ∧ 𝑛𝑍) → 𝑥 ∈ (𝐸𝑛))
149148ralrimiva 3113 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) → ∀𝑛𝑍 𝑥 ∈ (𝐸𝑛))
150 vex 3353 . . . . . . . . 9 𝑥 ∈ V
151 eliin 4683 . . . . . . . . 9 (𝑥 ∈ V → (𝑥 𝑛𝑍 (𝐸𝑛) ↔ ∀𝑛𝑍 𝑥 ∈ (𝐸𝑛)))
152150, 151ax-mp 5 . . . . . . . 8 (𝑥 𝑛𝑍 (𝐸𝑛) ↔ ∀𝑛𝑍 𝑥 ∈ (𝐸𝑛))
153149, 152sylibr 225 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐸𝐾) ∖ 𝐹)) → 𝑥 𝑛𝑍 (𝐸𝑛))
154153ssd 39906 . . . . . 6 (𝜑 → ((𝐸𝐾) ∖ 𝐹) ⊆ 𝑛𝑍 (𝐸𝑛))
155 ssid 3785 . . . . . . . . . . . 12 (𝐸𝐾) ⊆ (𝐸𝐾)
156155a1i 11 . . . . . . . . . . 11 (𝜑 → (𝐸𝐾) ⊆ (𝐸𝐾))
157 fveq2 6377 . . . . . . . . . . . . 13 (𝑛 = 𝐾 → (𝐸𝑛) = (𝐸𝐾))
158157sseq1d 3794 . . . . . . . . . . . 12 (𝑛 = 𝐾 → ((𝐸𝑛) ⊆ (𝐸𝐾) ↔ (𝐸𝐾) ⊆ (𝐸𝐾)))
159158rspcev 3462 . . . . . . . . . . 11 ((𝐾𝑍 ∧ (𝐸𝐾) ⊆ (𝐸𝐾)) → ∃𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
16015, 156, 159syl2anc 579 . . . . . . . . . 10 (𝜑 → ∃𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
161 iinss 4729 . . . . . . . . . 10 (∃𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾) → 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
162160, 161syl 17 . . . . . . . . 9 (𝜑 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
163162adantr 472 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝐾))
164 simpr 477 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑥 𝑛𝑍 (𝐸𝑛))
165163, 164sseldd 3764 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑥 ∈ (𝐸𝐾))
166 nfcv 2907 . . . . . . . . . . . . 13 𝑛𝑥
167 nfii1 4709 . . . . . . . . . . . . 13 𝑛 𝑛𝑍 (𝐸𝑛)
168166, 167nfel 2920 . . . . . . . . . . . 12 𝑛 𝑥 𝑛𝑍 (𝐸𝑛)
169 iinss2 4730 . . . . . . . . . . . . . . . 16 (𝑛𝑍 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝑛))
170169adantl 473 . . . . . . . . . . . . . . 15 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → 𝑛𝑍 (𝐸𝑛) ⊆ (𝐸𝑛))
171 simpl 474 . . . . . . . . . . . . . . 15 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → 𝑥 𝑛𝑍 (𝐸𝑛))
172170, 171sseldd 3764 . . . . . . . . . . . . . 14 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → 𝑥 ∈ (𝐸𝑛))
173 elndif 3898 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐸𝑛) → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
174172, 173syl 17 . . . . . . . . . . . . 13 ((𝑥 𝑛𝑍 (𝐸𝑛) ∧ 𝑛𝑍) → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
175174ex 401 . . . . . . . . . . . 12 (𝑥 𝑛𝑍 (𝐸𝑛) → (𝑛𝑍 → ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛))))
176168, 175ralrimi 3104 . . . . . . . . . . 11 (𝑥 𝑛𝑍 (𝐸𝑛) → ∀𝑛𝑍 ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
177 ralnex 3139 . . . . . . . . . . 11 (∀𝑛𝑍 ¬ 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)) ↔ ¬ ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
178176, 177sylib 209 . . . . . . . . . 10 (𝑥 𝑛𝑍 (𝐸𝑛) → ¬ ∃𝑛𝑍 𝑥 ∈ ((𝐸𝐾) ∖ (𝐸𝑛)))
179178, 137sylnibr 320 . . . . . . . . 9 (𝑥 𝑛𝑍 (𝐸𝑛) → ¬ 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
180179adantl 473 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → ¬ 𝑥 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
181142adantr 472 . . . . . . . 8 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝐹 = 𝑛𝑍 ((𝐸𝐾) ∖ (𝐸𝑛)))
182180, 181neleqtrrd 2866 . . . . . . 7 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → ¬ 𝑥𝐹)
183165, 182eldifd 3745 . . . . . 6 ((𝜑𝑥 𝑛𝑍 (𝐸𝑛)) → 𝑥 ∈ ((𝐸𝐾) ∖ 𝐹))
184154, 183eqelssd 3784 . . . . 5 (𝜑 → ((𝐸𝐾) ∖ 𝐹) = 𝑛𝑍 (𝐸𝑛))
185184fveq2d 6381 . . . 4 (𝜑 → (𝑀‘((𝐸𝐾) ∖ 𝐹)) = (𝑀 𝑛𝑍 (𝐸𝑛)))
186128, 185eqtr2d 2800 . . 3 (𝜑 → (𝑀 𝑛𝑍 (𝐸𝑛)) = ((𝑀‘(𝐸𝐾)) − (𝑀𝐹)))
187105, 186breq12d 4824 . 2 (𝜑 → (𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)) ↔ (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) ⇝ ((𝑀‘(𝐸𝐾)) − (𝑀𝐹))))
188103, 187mpbird 248 1 (𝜑𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  cdif 3731  cun 3732  cin 3733  wss 3734  c0 4081   ciun 4678   ciin 4679   class class class wbr 4811  cmpt 4890  dom cdm 5279  wf 6066  cfv 6070  (class class class)co 6844  ωcom 7265  cdom 8160  cc 10189  cr 10190  1c1 10192   + caddc 10194  cmin 10522  cz 11626  cuz 11889  ..^cfzo 12676  cli 14503  SAlgcsalg 41168  Meascmea 41306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-disj 4780  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-om 7266  df-1st 7368  df-2nd 7369  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-oadd 7770  df-omul 7771  df-er 7949  df-map 8064  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-sup 8557  df-oi 8624  df-card 9018  df-acn 9021  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-n0 11541  df-z 11627  df-uz 11890  df-rp 12032  df-xadd 12150  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-seq 13012  df-exp 13071  df-hash 13325  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-clim 14507  df-sum 14705  df-salg 41169  df-sumge0 41220  df-mea 41307
This theorem is referenced by:  meaiininc  41344
  Copyright terms: Public domain W3C validator