Metamath Proof Explorer


Theorem isomenndlem

Description: O is sub-additive w.r.t. countable indexed union, implies that O is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of Fremlin1 p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses isomenndlem.o φ O : 𝒫 X 0 +∞
isomenndlem.o0 φ O = 0
isomenndlem.y φ Y 𝒫 X
isomenndlem.subadd φ a : 𝒫 X O n a n sum^ n O a n
isomenndlem.b φ B
isomenndlem.f φ F : B 1-1 onto Y
isomenndlem.a A = n if n B F n
Assertion isomenndlem φ O Y sum^ O Y

Proof

Step Hyp Ref Expression
1 isomenndlem.o φ O : 𝒫 X 0 +∞
2 isomenndlem.o0 φ O = 0
3 isomenndlem.y φ Y 𝒫 X
4 isomenndlem.subadd φ a : 𝒫 X O n a n sum^ n O a n
5 isomenndlem.b φ B
6 isomenndlem.f φ F : B 1-1 onto Y
7 isomenndlem.a A = n if n B F n
8 id φ φ
9 iftrue n B if n B F n = F n
10 9 adantl φ n B if n B F n = F n
11 f1of F : B 1-1 onto Y F : B Y
12 6 11 syl φ F : B Y
13 ssun1 Y Y
14 13 a1i φ Y Y
15 12 14 fssd φ F : B Y
16 15 ffvelrnda φ n B F n Y
17 10 16 eqeltrd φ n B if n B F n Y
18 17 adantlr φ n n B if n B F n Y
19 iffalse ¬ n B if n B F n =
20 19 adantl φ ¬ n B if n B F n =
21 0ex V
22 21 snid
23 elun2 Y
24 22 23 ax-mp Y
25 24 a1i φ ¬ n B Y
26 20 25 eqeltrd φ ¬ n B if n B F n Y
27 26 adantlr φ n ¬ n B if n B F n Y
28 18 27 pm2.61dan φ n if n B F n Y
29 28 7 fmptd φ A : Y
30 0elpw 𝒫 X
31 snssi 𝒫 X 𝒫 X
32 30 31 ax-mp 𝒫 X
33 32 a1i φ 𝒫 X
34 3 33 unssd φ Y 𝒫 X
35 29 34 fssd φ A : 𝒫 X
36 nnex V
37 36 mptex n if n B F n V
38 7 37 eqeltri A V
39 feq1 a = A a : 𝒫 X A : 𝒫 X
40 39 anbi2d a = A φ a : 𝒫 X φ A : 𝒫 X
41 fveq1 a = A a n = A n
42 41 iuneq2d a = A n a n = n A n
43 42 fveq2d a = A O n a n = O n A n
44 simpl a = A n a = A
45 44 fveq1d a = A n a n = A n
46 45 fveq2d a = A n O a n = O A n
47 46 mpteq2dva a = A n O a n = n O A n
48 47 fveq2d a = A sum^ n O a n = sum^ n O A n
49 43 48 breq12d a = A O n a n sum^ n O a n O n A n sum^ n O A n
50 40 49 imbi12d a = A φ a : 𝒫 X O n a n sum^ n O a n φ A : 𝒫 X O n A n sum^ n O A n
51 38 50 4 vtocl φ A : 𝒫 X O n A n sum^ n O A n
52 8 35 51 syl2anc φ O n A n sum^ n O A n
53 12 ad2antrr φ B = n F : B Y
54 simpr B = n n
55 id B = B =
56 55 eqcomd B = = B
57 56 adantr B = n = B
58 54 57 eleqtrd B = n n B
59 58 adantll φ B = n n B
60 53 59 ffvelrnd φ B = n F n Y
61 eqid n F n = n F n
62 60 61 fmptd φ B = n F n : Y
63 7 a1i B = A = n if n B F n
64 58 iftrued B = n if n B F n = F n
65 64 mpteq2dva B = n if n B F n = n F n
66 63 65 eqtrd B = A = n F n
67 66 feq1d B = A : Y n F n : Y
68 67 adantl φ B = A : Y n F n : Y
69 62 68 mpbird φ B = A : Y
70 f1ofo F : B 1-1 onto Y F : B onto Y
71 6 70 syl φ F : B onto Y
72 dffo3 F : B onto Y F : B Y y Y n B y = F n
73 71 72 sylib φ F : B Y y Y n B y = F n
74 73 simprd φ y Y n B y = F n
75 74 adantr φ y Y y Y n B y = F n
76 simpr φ y Y y Y
77 rspa y Y n B y = F n y Y n B y = F n
78 75 76 77 syl2anc φ y Y n B y = F n
79 78 adantlr φ B = y Y n B y = F n
80 nfv n φ B =
81 nfre1 n n y = A n
82 simpr B = n B n B
83 simpl B = n B B =
84 82 83 eleqtrd B = n B n
85 84 adantll φ B = n B n
86 85 3adant3 φ B = n B y = F n n
87 63 fveq1d B = A n = n if n B F n n
88 87 3ad2ant1 B = n B y = F n A n = n if n B F n n
89 fvex F n V
90 89 21 ifex if n B F n V
91 90 a1i B = n B if n B F n V
92 eqid n if n B F n = n if n B F n
93 92 fvmpt2 n if n B F n V n if n B F n n = if n B F n
94 84 91 93 syl2anc B = n B n if n B F n n = if n B F n
95 9 adantl B = n B if n B F n = F n
96 94 95 eqtrd B = n B n if n B F n n = F n
97 96 3adant3 B = n B y = F n n if n B F n n = F n
98 id y = F n y = F n
99 98 eqcomd y = F n F n = y
100 99 3ad2ant3 B = n B y = F n F n = y
101 88 97 100 3eqtrrd B = n B y = F n y = A n
102 101 3adant1l φ B = n B y = F n y = A n
103 rspe n y = A n n y = A n
104 86 102 103 syl2anc φ B = n B y = F n n y = A n
105 104 3exp φ B = n B y = F n n y = A n
106 80 81 105 rexlimd φ B = n B y = F n n y = A n
107 106 adantr φ B = y Y n B y = F n n y = A n
108 79 107 mpd φ B = y Y n y = A n
109 108 ralrimiva φ B = y Y n y = A n
110 69 109 jca φ B = A : Y y Y n y = A n
111 dffo3 A : onto Y A : Y y Y n y = A n
112 110 111 sylibr φ B = A : onto Y
113 founiiun A : onto Y Y = n A n
114 112 113 syl φ B = Y = n A n
115 uniun Y = Y
116 21 unisn =
117 116 uneq2i Y = Y
118 un0 Y = Y
119 115 117 118 3eqtrri Y = Y
120 119 a1i φ ¬ B = Y = Y
121 29 adantr φ ¬ B = A : Y
122 nfv n φ ¬ B = y =
123 5 adantr φ ¬ B = B
124 55 necon3bi ¬ B = B
125 124 adantl φ ¬ B = B
126 123 125 jca φ ¬ B = B B
127 df-pss B B B
128 126 127 sylibr φ ¬ B = B
129 pssnel B n n ¬ n B
130 128 129 syl φ ¬ B = n n ¬ n B
131 130 adantr φ ¬ B = y = n n ¬ n B
132 simprl φ y = n ¬ n B n
133 simprl φ n ¬ n B n
134 90 a1i φ n ¬ n B if n B F n V
135 7 fvmpt2 n if n B F n V A n = if n B F n
136 133 134 135 syl2anc φ n ¬ n B A n = if n B F n
137 136 adantlr φ y = n ¬ n B A n = if n B F n
138 19 ad2antll φ y = n ¬ n B if n B F n =
139 id y = y =
140 139 eqcomd y = = y
141 140 ad2antlr φ y = n ¬ n B = y
142 137 138 141 3eqtrrd φ y = n ¬ n B y = A n
143 132 142 103 syl2anc φ y = n ¬ n B n y = A n
144 143 ex φ y = n ¬ n B n y = A n
145 144 adantlr φ ¬ B = y = n ¬ n B n y = A n
146 122 81 131 145 exlimimdd φ ¬ B = y = n y = A n
147 146 adantlr φ ¬ B = y Y y = n y = A n
148 simplll φ ¬ B = y Y ¬ y = φ
149 simpl y Y ¬ y = y Y
150 elsni y y =
151 150 con3i ¬ y = ¬ y
152 151 adantl y Y ¬ y = ¬ y
153 elunnel2 y Y ¬ y y Y
154 149 152 153 syl2anc y Y ¬ y = y Y
155 154 adantll φ ¬ B = y Y ¬ y = y Y
156 71 adantr φ y Y F : B onto Y
157 foelrni F : B onto Y y Y n B F n = y
158 156 76 157 syl2anc φ y Y n B F n = y
159 nfv n φ y Y
160 5 sselda φ n B n
161 160 3adant3 φ n B F n = y n
162 160 90 135 sylancl φ n B A n = if n B F n
163 162 10 eqtrd φ n B A n = F n
164 163 3adant3 φ n B F n = y A n = F n
165 simp3 φ n B F n = y F n = y
166 164 165 eqtr2d φ n B F n = y y = A n
167 161 166 103 syl2anc φ n B F n = y n y = A n
168 167 3exp φ n B F n = y n y = A n
169 168 adantr φ y Y n B F n = y n y = A n
170 159 81 169 rexlimd φ y Y n B F n = y n y = A n
171 158 170 mpd φ y Y n y = A n
172 148 155 171 syl2anc φ ¬ B = y Y ¬ y = n y = A n
173 147 172 pm2.61dan φ ¬ B = y Y n y = A n
174 173 ralrimiva φ ¬ B = y Y n y = A n
175 121 174 jca φ ¬ B = A : Y y Y n y = A n
176 dffo3 A : onto Y A : Y y Y n y = A n
177 175 176 sylibr φ ¬ B = A : onto Y
178 founiiun A : onto Y Y = n A n
179 177 178 syl φ ¬ B = Y = n A n
180 120 179 eqtrd φ ¬ B = Y = n A n
181 114 180 pm2.61dan φ Y = n A n
182 181 fveq2d φ O Y = O n A n
183 uncom B B = B B
184 183 a1i φ B B = B B
185 undif B B B =
186 5 185 sylib φ B B =
187 184 186 eqtrd φ B B =
188 187 eqcomd φ = B B
189 188 mpteq1d φ n O A n = n B B O A n
190 189 fveq2d φ sum^ n O A n = sum^ n B B O A n
191 nfv n φ
192 difexg V B V
193 36 192 ax-mp B V
194 193 a1i φ B V
195 36 a1i φ V
196 195 5 ssexd φ B V
197 disjdifr B B =
198 197 a1i φ B B =
199 simpl φ n B φ
200 eldifi n B n
201 200 adantl φ n B n
202 1 adantr φ n O : 𝒫 X 0 +∞
203 35 ffvelrnda φ n A n 𝒫 X
204 202 203 ffvelrnd φ n O A n 0 +∞
205 199 201 204 syl2anc φ n B O A n 0 +∞
206 160 204 syldan φ n B O A n 0 +∞
207 191 194 196 198 205 206 sge0splitmpt φ sum^ n B B O A n = sum^ n B O A n + 𝑒 sum^ n B O A n
208 eqid n B O A n = n B O A n
209 206 208 fmptd φ n B O A n : B 0 +∞
210 196 209 sge0xrcl φ sum^ n B O A n *
211 210 xaddid2d φ 0 + 𝑒 sum^ n B O A n = sum^ n B O A n
212 90 a1i φ n B if n B F n V
213 201 212 135 syl2anc φ n B A n = if n B F n
214 eldifn n B ¬ n B
215 214 adantl φ n B ¬ n B
216 215 iffalsed φ n B if n B F n =
217 213 216 eqtrd φ n B A n =
218 217 fveq2d φ n B O A n = O
219 199 2 syl φ n B O = 0
220 218 219 eqtrd φ n B O A n = 0
221 220 mpteq2dva φ n B O A n = n B 0
222 221 fveq2d φ sum^ n B O A n = sum^ n B 0
223 191 194 sge0z φ sum^ n B 0 = 0
224 222 223 eqtrd φ sum^ n B O A n = 0
225 224 oveq1d φ sum^ n B O A n + 𝑒 sum^ n B O A n = 0 + 𝑒 sum^ n B O A n
226 1 3 feqresmpt φ O Y = y Y O y
227 226 fveq2d φ sum^ O Y = sum^ y Y O y
228 nfv y φ
229 fveq2 y = A n O y = O A n
230 163 eqcomd φ n B F n = A n
231 1 adantr φ y Y O : 𝒫 X 0 +∞
232 3 sselda φ y Y y 𝒫 X
233 231 232 ffvelrnd φ y Y O y 0 +∞
234 228 191 229 196 6 230 233 sge0f1o φ sum^ y Y O y = sum^ n B O A n
235 eqidd φ sum^ n B O A n = sum^ n B O A n
236 227 234 235 3eqtrd φ sum^ O Y = sum^ n B O A n
237 211 225 236 3eqtr4d φ sum^ n B O A n + 𝑒 sum^ n B O A n = sum^ O Y
238 190 207 237 3eqtrrd φ sum^ O Y = sum^ n O A n
239 182 238 breq12d φ O Y sum^ O Y O n A n sum^ n O A n
240 52 239 mpbird φ O Y sum^ O Y