# Metamath Proof Explorer

## Theorem meaiininclem

Description: Measures are continuous from above: if E 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)

Ref Expression
Hypotheses meaiininclem.m ${⊢}{\phi }\to {M}\in \mathrm{Meas}$
meaiininclem.n ${⊢}{\phi }\to {N}\in ℤ$
meaiininclem.z ${⊢}{Z}={ℤ}_{\ge {N}}$
meaiininclem.e ${⊢}{\phi }\to {E}:{Z}⟶\mathrm{dom}{M}$
meaiininclem.i ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({n}+1\right)\subseteq {E}\left({n}\right)$
meaiininclem.k ${⊢}{\phi }\to {K}\in {ℤ}_{\ge {N}}$
meaiininclem.r ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\right)\in ℝ$
meaiininclem.s ${⊢}{S}=\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)$
meaiininclem.g ${⊢}{G}=\left({n}\in {Z}⟼{E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
meaiininclem.f ${⊢}{F}=\bigcup _{{n}\in {Z}}{G}\left({n}\right)$
Assertion meaiininclem ${⊢}{\phi }\to {S}⇝{M}\left(\bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)$

### Proof

Step Hyp Ref Expression
1 meaiininclem.m ${⊢}{\phi }\to {M}\in \mathrm{Meas}$
2 meaiininclem.n ${⊢}{\phi }\to {N}\in ℤ$
3 meaiininclem.z ${⊢}{Z}={ℤ}_{\ge {N}}$
4 meaiininclem.e ${⊢}{\phi }\to {E}:{Z}⟶\mathrm{dom}{M}$
5 meaiininclem.i ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({n}+1\right)\subseteq {E}\left({n}\right)$
6 meaiininclem.k ${⊢}{\phi }\to {K}\in {ℤ}_{\ge {N}}$
7 meaiininclem.r ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\right)\in ℝ$
8 meaiininclem.s ${⊢}{S}=\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)$
9 meaiininclem.g ${⊢}{G}=\left({n}\in {Z}⟼{E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
10 meaiininclem.f ${⊢}{F}=\bigcup _{{n}\in {Z}}{G}\left({n}\right)$
11 uzss ${⊢}{K}\in {ℤ}_{\ge {N}}\to {ℤ}_{\ge {K}}\subseteq {ℤ}_{\ge {N}}$
12 6 11 syl ${⊢}{\phi }\to {ℤ}_{\ge {K}}\subseteq {ℤ}_{\ge {N}}$
13 12 3 sseqtrrdi ${⊢}{\phi }\to {ℤ}_{\ge {K}}\subseteq {Z}$
14 13 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {ℤ}_{\ge {K}}\subseteq {Z}$
15 simpr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {n}\in {ℤ}_{\ge {K}}$
16 14 15 sseldd ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {n}\in {Z}$
17 9 a1i ${⊢}{\phi }\to {G}=\left({n}\in {Z}⟼{E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
18 eqid ${⊢}\mathrm{dom}{M}=\mathrm{dom}{M}$
19 1 18 dmmeasal ${⊢}{\phi }\to \mathrm{dom}{M}\in \mathrm{SAlg}$
20 19 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \mathrm{dom}{M}\in \mathrm{SAlg}$
21 6 3 eleqtrrdi ${⊢}{\phi }\to {K}\in {Z}$
22 4 ffvelrnda ${⊢}\left({\phi }\wedge {K}\in {Z}\right)\to {E}\left({K}\right)\in \mathrm{dom}{M}$
23 21 22 mpdan ${⊢}{\phi }\to {E}\left({K}\right)\in \mathrm{dom}{M}$
24 23 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({K}\right)\in \mathrm{dom}{M}$
25 4 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({n}\right)\in \mathrm{dom}{M}$
26 saldifcl2 ${⊢}\left(\mathrm{dom}{M}\in \mathrm{SAlg}\wedge {E}\left({K}\right)\in \mathrm{dom}{M}\wedge {E}\left({n}\right)\in \mathrm{dom}{M}\right)\to {E}\left({K}\right)\setminus {E}\left({n}\right)\in \mathrm{dom}{M}$
27 20 24 25 26 syl3anc ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({K}\right)\setminus {E}\left({n}\right)\in \mathrm{dom}{M}$
28 27 elexd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({K}\right)\setminus {E}\left({n}\right)\in \mathrm{V}$
29 17 28 fvmpt2d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {G}\left({n}\right)={E}\left({K}\right)\setminus {E}\left({n}\right)$
30 16 29 syldan ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {G}\left({n}\right)={E}\left({K}\right)\setminus {E}\left({n}\right)$
31 30 fveq2d ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({G}\left({n}\right)\right)={M}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
32 1 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\in \mathrm{Meas}$
33 23 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {E}\left({K}\right)\in \mathrm{dom}{M}$
34 7 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({K}\right)\right)\in ℝ$
35 16 25 syldan ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {E}\left({n}\right)\in \mathrm{dom}{M}$
36 simpl ${⊢}\left({\phi }\wedge {m}\in \left({K}..^{n}\right)\right)\to {\phi }$
37 36 13 syl ${⊢}\left({\phi }\wedge {m}\in \left({K}..^{n}\right)\right)\to {ℤ}_{\ge {K}}\subseteq {Z}$
38 elfzouz ${⊢}{m}\in \left({K}..^{n}\right)\to {m}\in {ℤ}_{\ge {K}}$
39 38 adantl ${⊢}\left({\phi }\wedge {m}\in \left({K}..^{n}\right)\right)\to {m}\in {ℤ}_{\ge {K}}$
40 37 39 sseldd ${⊢}\left({\phi }\wedge {m}\in \left({K}..^{n}\right)\right)\to {m}\in {Z}$
41 eleq1w ${⊢}{n}={m}\to \left({n}\in {Z}↔{m}\in {Z}\right)$
42 41 anbi2d ${⊢}{n}={m}\to \left(\left({\phi }\wedge {n}\in {Z}\right)↔\left({\phi }\wedge {m}\in {Z}\right)\right)$
43 fvoveq1 ${⊢}{n}={m}\to {E}\left({n}+1\right)={E}\left({m}+1\right)$
44 fveq2 ${⊢}{n}={m}\to {E}\left({n}\right)={E}\left({m}\right)$
45 43 44 sseq12d ${⊢}{n}={m}\to \left({E}\left({n}+1\right)\subseteq {E}\left({n}\right)↔{E}\left({m}+1\right)\subseteq {E}\left({m}\right)\right)$
46 42 45 imbi12d ${⊢}{n}={m}\to \left(\left(\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({n}+1\right)\subseteq {E}\left({n}\right)\right)↔\left(\left({\phi }\wedge {m}\in {Z}\right)\to {E}\left({m}+1\right)\subseteq {E}\left({m}\right)\right)\right)$
47 46 5 chvarvv ${⊢}\left({\phi }\wedge {m}\in {Z}\right)\to {E}\left({m}+1\right)\subseteq {E}\left({m}\right)$
48 36 40 47 syl2anc ${⊢}\left({\phi }\wedge {m}\in \left({K}..^{n}\right)\right)\to {E}\left({m}+1\right)\subseteq {E}\left({m}\right)$
49 48 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\wedge {m}\in \left({K}..^{n}\right)\right)\to {E}\left({m}+1\right)\subseteq {E}\left({m}\right)$
50 15 49 ssdec ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {E}\left({n}\right)\subseteq {E}\left({K}\right)$
51 32 33 34 35 50 meadif ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)={M}\left({E}\left({K}\right)\right)-{M}\left({E}\left({n}\right)\right)$
52 31 51 eqtrd ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({G}\left({n}\right)\right)={M}\left({E}\left({K}\right)\right)-{M}\left({E}\left({n}\right)\right)$
53 52 oveq2d ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({K}\right)\right)-{M}\left({G}\left({n}\right)\right)={M}\left({E}\left({K}\right)\right)-\left({M}\left({E}\left({K}\right)\right)-{M}\left({E}\left({n}\right)\right)\right)$
54 7 recnd ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\right)\in ℂ$
55 54 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({K}\right)\right)\in ℂ$
56 32 33 34 50 35 meassre ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({n}\right)\right)\in ℝ$
57 56 recnd ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({n}\right)\right)\in ℂ$
58 55 57 nncand ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({K}\right)\right)-\left({M}\left({E}\left({K}\right)\right)-{M}\left({E}\left({n}\right)\right)\right)={M}\left({E}\left({n}\right)\right)$
59 53 58 eqtr2d ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({E}\left({n}\right)\right)={M}\left({E}\left({K}\right)\right)-{M}\left({G}\left({n}\right)\right)$
60 59 mpteq2dva ${⊢}{\phi }\to \left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({n}\right)\right)\right)=\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({K}\right)\right)-{M}\left({G}\left({n}\right)\right)\right)$
61 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
62 eqid ${⊢}{ℤ}_{\ge {K}}={ℤ}_{\ge {K}}$
63 6 eluzelzd ${⊢}{\phi }\to {K}\in ℤ$
64 difssd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({K}\right)\setminus {E}\left({n}\right)\subseteq {E}\left({K}\right)$
65 29 64 eqsstrd ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {G}\left({n}\right)\subseteq {E}\left({K}\right)$
66 16 65 syldan ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {G}\left({n}\right)\subseteq {E}\left({K}\right)$
67 27 9 fmptd ${⊢}{\phi }\to {G}:{Z}⟶\mathrm{dom}{M}$
68 67 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {G}\left({n}\right)\in \mathrm{dom}{M}$
69 16 68 syldan ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {G}\left({n}\right)\in \mathrm{dom}{M}$
70 32 33 34 66 69 meassre ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({G}\left({n}\right)\right)\in ℝ$
71 70 recnd ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {K}}\right)\to {M}\left({G}\left({n}\right)\right)\in ℂ$
72 5 sscond ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({K}\right)\setminus {E}\left({n}\right)\subseteq {E}\left({K}\right)\setminus {E}\left({n}+1\right)$
73 44 difeq2d ${⊢}{n}={m}\to {E}\left({K}\right)\setminus {E}\left({n}\right)={E}\left({K}\right)\setminus {E}\left({m}\right)$
74 73 cbvmptv ${⊢}\left({n}\in {Z}⟼{E}\left({K}\right)\setminus {E}\left({n}\right)\right)=\left({m}\in {Z}⟼{E}\left({K}\right)\setminus {E}\left({m}\right)\right)$
75 9 74 eqtri ${⊢}{G}=\left({m}\in {Z}⟼{E}\left({K}\right)\setminus {E}\left({m}\right)\right)$
76 fveq2 ${⊢}{m}={n}+1\to {E}\left({m}\right)={E}\left({n}+1\right)$
77 76 difeq2d ${⊢}{m}={n}+1\to {E}\left({K}\right)\setminus {E}\left({m}\right)={E}\left({K}\right)\setminus {E}\left({n}+1\right)$
78 3 peano2uzs ${⊢}{n}\in {Z}\to {n}+1\in {Z}$
79 78 adantl ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {n}+1\in {Z}$
80 fvex ${⊢}{E}\left({K}\right)\in \mathrm{V}$
81 80 difexi ${⊢}{E}\left({K}\right)\setminus {E}\left({n}+1\right)\in \mathrm{V}$
82 81 a1i ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {E}\left({K}\right)\setminus {E}\left({n}+1\right)\in \mathrm{V}$
83 75 77 79 82 fvmptd3 ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {G}\left({n}+1\right)={E}\left({K}\right)\setminus {E}\left({n}+1\right)$
84 29 83 sseq12d ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to \left({G}\left({n}\right)\subseteq {G}\left({n}+1\right)↔{E}\left({K}\right)\setminus {E}\left({n}\right)\subseteq {E}\left({K}\right)\setminus {E}\left({n}+1\right)\right)$
85 72 84 mpbird ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {G}\left({n}\right)\subseteq {G}\left({n}+1\right)$
86 1 adantr ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {M}\in \mathrm{Meas}$
87 86 18 68 24 65 meassle ${⊢}\left({\phi }\wedge {n}\in {Z}\right)\to {M}\left({G}\left({n}\right)\right)\le {M}\left({E}\left({K}\right)\right)$
88 eqid ${⊢}\left({n}\in {Z}⟼{M}\left({G}\left({n}\right)\right)\right)=\left({n}\in {Z}⟼{M}\left({G}\left({n}\right)\right)\right)$
89 1 2 3 67 85 7 87 88 meaiuninc2 ${⊢}{\phi }\to \left({n}\in {Z}⟼{M}\left({G}\left({n}\right)\right)\right)⇝{M}\left(\bigcup _{{n}\in {Z}}{G}\left({n}\right)\right)$
90 eqid ${⊢}\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({G}\left({n}\right)\right)\right)=\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({G}\left({n}\right)\right)\right)$
91 3 88 21 90 climresmpt ${⊢}{\phi }\to \left(\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({G}\left({n}\right)\right)\right)⇝{M}\left(\bigcup _{{n}\in {Z}}{G}\left({n}\right)\right)↔\left({n}\in {Z}⟼{M}\left({G}\left({n}\right)\right)\right)⇝{M}\left(\bigcup _{{n}\in {Z}}{G}\left({n}\right)\right)\right)$
92 89 91 mpbird ${⊢}{\phi }\to \left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({G}\left({n}\right)\right)\right)⇝{M}\left(\bigcup _{{n}\in {Z}}{G}\left({n}\right)\right)$
93 10 eqcomi ${⊢}\bigcup _{{n}\in {Z}}{G}\left({n}\right)={F}$
94 93 fveq2i ${⊢}{M}\left(\bigcup _{{n}\in {Z}}{G}\left({n}\right)\right)={M}\left({F}\right)$
95 94 a1i ${⊢}{\phi }\to {M}\left(\bigcup _{{n}\in {Z}}{G}\left({n}\right)\right)={M}\left({F}\right)$
96 92 95 breqtrd ${⊢}{\phi }\to \left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({G}\left({n}\right)\right)\right)⇝{M}\left({F}\right)$
97 61 62 63 54 71 96 climsubc1mpt ${⊢}{\phi }\to \left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({K}\right)\right)-{M}\left({G}\left({n}\right)\right)\right)⇝\left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)\right)$
98 60 97 eqbrtrd ${⊢}{\phi }\to \left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({n}\right)\right)\right)⇝\left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)\right)$
99 eqid ${⊢}\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)=\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)$
100 eqid ${⊢}\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({n}\right)\right)\right)=\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({n}\right)\right)\right)$
101 3 99 21 100 climresmpt ${⊢}{\phi }\to \left(\left({n}\in {ℤ}_{\ge {K}}⟼{M}\left({E}\left({n}\right)\right)\right)⇝\left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)\right)↔\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)⇝\left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)\right)\right)$
102 98 101 mpbid ${⊢}{\phi }\to \left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)⇝\left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)\right)$
103 8 a1i ${⊢}{\phi }\to {S}=\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)$
104 eqidd ${⊢}{\phi }\to {M}\left({F}\cup \left({E}\left({K}\right)\setminus {F}\right)\right)={M}\left({F}\cup \left({E}\left({K}\right)\setminus {F}\right)\right)$
105 3 uzct ${⊢}{Z}\preccurlyeq \mathrm{\omega }$
106 105 a1i ${⊢}{\phi }\to {Z}\preccurlyeq \mathrm{\omega }$
107 19 106 68 saliuncl ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}{G}\left({n}\right)\in \mathrm{dom}{M}$
108 10 107 eqeltrid ${⊢}{\phi }\to {F}\in \mathrm{dom}{M}$
109 saldifcl2 ${⊢}\left(\mathrm{dom}{M}\in \mathrm{SAlg}\wedge {E}\left({K}\right)\in \mathrm{dom}{M}\wedge {F}\in \mathrm{dom}{M}\right)\to {E}\left({K}\right)\setminus {F}\in \mathrm{dom}{M}$
110 19 23 108 109 syl3anc ${⊢}{\phi }\to {E}\left({K}\right)\setminus {F}\in \mathrm{dom}{M}$
111 disjdif ${⊢}{F}\cap \left({E}\left({K}\right)\setminus {F}\right)=\varnothing$
112 111 a1i ${⊢}{\phi }\to {F}\cap \left({E}\left({K}\right)\setminus {F}\right)=\varnothing$
113 65 iunssd ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}{G}\left({n}\right)\subseteq {E}\left({K}\right)$
114 10 113 eqsstrid ${⊢}{\phi }\to {F}\subseteq {E}\left({K}\right)$
115 1 23 7 114 108 meassre ${⊢}{\phi }\to {M}\left({F}\right)\in ℝ$
116 difssd ${⊢}{\phi }\to {E}\left({K}\right)\setminus {F}\subseteq {E}\left({K}\right)$
117 1 23 7 116 110 meassre ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\setminus {F}\right)\in ℝ$
118 1 18 108 110 112 115 117 meadjunre ${⊢}{\phi }\to {M}\left({F}\cup \left({E}\left({K}\right)\setminus {F}\right)\right)={M}\left({F}\right)+{M}\left({E}\left({K}\right)\setminus {F}\right)$
119 undif ${⊢}{F}\subseteq {E}\left({K}\right)↔{F}\cup \left({E}\left({K}\right)\setminus {F}\right)={E}\left({K}\right)$
120 114 119 sylib ${⊢}{\phi }\to {F}\cup \left({E}\left({K}\right)\setminus {F}\right)={E}\left({K}\right)$
121 120 fveq2d ${⊢}{\phi }\to {M}\left({F}\cup \left({E}\left({K}\right)\setminus {F}\right)\right)={M}\left({E}\left({K}\right)\right)$
122 104 118 121 3eqtr3d ${⊢}{\phi }\to {M}\left({F}\right)+{M}\left({E}\left({K}\right)\setminus {F}\right)={M}\left({E}\left({K}\right)\right)$
123 115 recnd ${⊢}{\phi }\to {M}\left({F}\right)\in ℂ$
124 117 recnd ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\setminus {F}\right)\in ℂ$
125 54 123 124 subaddd ${⊢}{\phi }\to \left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)={M}\left({E}\left({K}\right)\setminus {F}\right)↔{M}\left({F}\right)+{M}\left({E}\left({K}\right)\setminus {F}\right)={M}\left({E}\left({K}\right)\right)\right)$
126 122 125 mpbird ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)={M}\left({E}\left({K}\right)\setminus {F}\right)$
127 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {x}\in \left({E}\left({K}\right)\setminus {F}\right)$
128 simplr ${⊢}\left(\left({x}\in \left({E}\left({K}\right)\setminus {F}\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {n}\in {Z}$
129 eldifi ${⊢}{x}\in \left({E}\left({K}\right)\setminus {F}\right)\to {x}\in {E}\left({K}\right)$
130 129 ad2antrr ${⊢}\left(\left({x}\in \left({E}\left({K}\right)\setminus {F}\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {x}\in {E}\left({K}\right)$
131 simpr ${⊢}\left(\left({x}\in \left({E}\left({K}\right)\setminus {F}\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to ¬{x}\in {E}\left({n}\right)$
132 130 131 eldifd ${⊢}\left(\left({x}\in \left({E}\left({K}\right)\setminus {F}\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
133 rspe ${⊢}\left({n}\in {Z}\wedge {x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
134 128 132 133 syl2anc ${⊢}\left(\left({x}\in \left({E}\left({K}\right)\setminus {F}\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
135 eliun ${⊢}{x}\in \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)↔\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
136 134 135 sylibr ${⊢}\left(\left({x}\in \left({E}\left({K}\right)\setminus {F}\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {x}\in \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
137 136 adantlll ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {x}\in \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
138 10 a1i ${⊢}{\phi }\to {F}=\bigcup _{{n}\in {Z}}{G}\left({n}\right)$
139 29 iuneq2dv ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}{G}\left({n}\right)=\bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
140 138 139 eqtrd ${⊢}{\phi }\to {F}=\bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
141 140 eqcomd ${⊢}{\phi }\to \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)={F}$
142 141 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)={F}$
143 137 142 eleqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to {x}\in {F}$
144 elndif ${⊢}{x}\in {F}\to ¬{x}\in \left({E}\left({K}\right)\setminus {F}\right)$
145 143 144 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\wedge {n}\in {Z}\right)\wedge ¬{x}\in {E}\left({n}\right)\right)\to ¬{x}\in \left({E}\left({K}\right)\setminus {F}\right)$
146 127 145 condan ${⊢}\left(\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\wedge {n}\in {Z}\right)\to {x}\in {E}\left({n}\right)$
147 146 ralrimiva ${⊢}\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\to \forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in {E}\left({n}\right)$
148 vex ${⊢}{x}\in \mathrm{V}$
149 eliin ${⊢}{x}\in \mathrm{V}\to \left({x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)↔\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in {E}\left({n}\right)\right)$
150 148 149 ax-mp ${⊢}{x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)↔\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in {E}\left({n}\right)$
151 147 150 sylibr ${⊢}\left({\phi }\wedge {x}\in \left({E}\left({K}\right)\setminus {F}\right)\right)\to {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)$
152 151 ssd ${⊢}{\phi }\to {E}\left({K}\right)\setminus {F}\subseteq \bigcap _{{n}\in {Z}}{E}\left({n}\right)$
153 ssid ${⊢}{E}\left({K}\right)\subseteq {E}\left({K}\right)$
154 153 a1i ${⊢}{\phi }\to {E}\left({K}\right)\subseteq {E}\left({K}\right)$
155 fveq2 ${⊢}{n}={K}\to {E}\left({n}\right)={E}\left({K}\right)$
156 155 sseq1d ${⊢}{n}={K}\to \left({E}\left({n}\right)\subseteq {E}\left({K}\right)↔{E}\left({K}\right)\subseteq {E}\left({K}\right)\right)$
157 156 rspcev ${⊢}\left({K}\in {Z}\wedge {E}\left({K}\right)\subseteq {E}\left({K}\right)\right)\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{E}\left({n}\right)\subseteq {E}\left({K}\right)$
158 21 154 157 syl2anc ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{E}\left({n}\right)\subseteq {E}\left({K}\right)$
159 iinss ${⊢}\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{E}\left({n}\right)\subseteq {E}\left({K}\right)\to \bigcap _{{n}\in {Z}}{E}\left({n}\right)\subseteq {E}\left({K}\right)$
160 158 159 syl ${⊢}{\phi }\to \bigcap _{{n}\in {Z}}{E}\left({n}\right)\subseteq {E}\left({K}\right)$
161 160 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to \bigcap _{{n}\in {Z}}{E}\left({n}\right)\subseteq {E}\left({K}\right)$
162 simpr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)$
163 161 162 sseldd ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to {x}\in {E}\left({K}\right)$
164 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{x}$
165 nfii1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\bigcap _{{n}\in {Z}}{E}\left({n}\right)$
166 164 165 nfel ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)$
167 iinss2 ${⊢}{n}\in {Z}\to \bigcap _{{n}\in {Z}}{E}\left({n}\right)\subseteq {E}\left({n}\right)$
168 167 adantl ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\wedge {n}\in {Z}\right)\to \bigcap _{{n}\in {Z}}{E}\left({n}\right)\subseteq {E}\left({n}\right)$
169 simpl ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\wedge {n}\in {Z}\right)\to {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)$
170 168 169 sseldd ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\wedge {n}\in {Z}\right)\to {x}\in {E}\left({n}\right)$
171 elndif ${⊢}{x}\in {E}\left({n}\right)\to ¬{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
172 170 171 syl ${⊢}\left({x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\wedge {n}\in {Z}\right)\to ¬{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
173 172 ex ${⊢}{x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\to \left({n}\in {Z}\to ¬{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)\right)$
174 166 173 ralrimi ${⊢}{x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\to \forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}¬{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
175 ralnex ${⊢}\forall {n}\in {Z}\phantom{\rule{.4em}{0ex}}¬{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)↔¬\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
176 174 175 sylib ${⊢}{x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\to ¬\exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}{x}\in \left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
177 176 135 sylnibr ${⊢}{x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\to ¬{x}\in \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
178 177 adantl ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to ¬{x}\in \bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
179 140 adantr ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to {F}=\bigcup _{{n}\in {Z}}\left({E}\left({K}\right)\setminus {E}\left({n}\right)\right)$
180 178 179 neleqtrrd ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to ¬{x}\in {F}$
181 163 180 eldifd ${⊢}\left({\phi }\wedge {x}\in \bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)\to {x}\in \left({E}\left({K}\right)\setminus {F}\right)$
182 152 181 eqelssd ${⊢}{\phi }\to {E}\left({K}\right)\setminus {F}=\bigcap _{{n}\in {Z}}{E}\left({n}\right)$
183 182 fveq2d ${⊢}{\phi }\to {M}\left({E}\left({K}\right)\setminus {F}\right)={M}\left(\bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)$
184 126 183 eqtr2d ${⊢}{\phi }\to {M}\left(\bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)={M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)$
185 103 184 breq12d ${⊢}{\phi }\to \left({S}⇝{M}\left(\bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)↔\left({n}\in {Z}⟼{M}\left({E}\left({n}\right)\right)\right)⇝\left({M}\left({E}\left({K}\right)\right)-{M}\left({F}\right)\right)\right)$
186 102 185 mpbird ${⊢}{\phi }\to {S}⇝{M}\left(\bigcap _{{n}\in {Z}}{E}\left({n}\right)\right)$