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 
|- ( ph -> M e. Meas )
meaiininclem.n 
|- ( ph -> N e. ZZ )
meaiininclem.z 
|- Z = ( ZZ>= ` N )
meaiininclem.e 
|- ( ph -> E : Z --> dom M )
meaiininclem.i 
|- ( ( ph /\ n e. Z ) -> ( E ` ( n + 1 ) ) C_ ( E ` n ) )
meaiininclem.k 
|- ( ph -> K e. ( ZZ>= ` N ) )
meaiininclem.r 
|- ( ph -> ( M ` ( E ` K ) ) e. RR )
meaiininclem.s 
|- S = ( n e. Z |-> ( M ` ( E ` n ) ) )
meaiininclem.g 
|- G = ( n e. Z |-> ( ( E ` K ) \ ( E ` n ) ) )
meaiininclem.f 
|- F = U_ n e. Z ( G ` n )
Assertion meaiininclem 
|- ( ph -> S ~~> ( M ` |^|_ n e. Z ( E ` n ) ) )

Proof

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