Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sibfof Unicode version

Theorem sibfof 24607
 Description: Applying function operations on simple functions results in simple functions with regard to the the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.)
Hypotheses
Ref Expression
sitgval.b
sitgval.j
sitgval.s sigaGen
sitgval.0
sitgval.x
sitgval.h RRHomScalar
sitgval.1
sitgval.2 measures
sibfmbl.1 sitg
sibfof.c
sibfof.0
sibfof.1
sibfof.2 sitg
sibfof.3
sibfof.4
sibfof.5
Assertion
Ref Expression
sibfof sitg

Proof of Theorem sibfof
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sibfof.1 . . . . . . . . . 10
2 sibfof.0 . . . . . . . . . . . . 13
3 sitgval.b . . . . . . . . . . . . . 14
4 sitgval.j . . . . . . . . . . . . . 14
53, 4tpsuni 16958 . . . . . . . . . . . . 13
62, 5syl 16 . . . . . . . . . . . 12
76, 6xpeq12d 4862 . . . . . . . . . . 11
87feq2d 5540 . . . . . . . . . 10
91, 8mpbid 202 . . . . . . . . 9
109fovrnda 6176 . . . . . . . 8
11 sitgval.s . . . . . . . . 9 sigaGen
12 sitgval.0 . . . . . . . . 9
13 sitgval.x . . . . . . . . 9
14 sitgval.h . . . . . . . . 9 RRHomScalar
15 sitgval.1 . . . . . . . . 9
16 sitgval.2 . . . . . . . . 9 measures
17 sibfmbl.1 . . . . . . . . 9 sitg
183, 4, 11, 12, 13, 14, 15, 16, 17sibff 24604 . . . . . . . 8
19 sibfof.2 . . . . . . . . 9 sitg
203, 4, 11, 12, 13, 14, 15, 16, 19sibff 24604 . . . . . . . 8
21 dmexg 5089 . . . . . . . . 9 measures
22 uniexg 4665 . . . . . . . . 9
2316, 21, 223syl 19 . . . . . . . 8
24 inidm 3510 . . . . . . . 8
2510, 18, 20, 23, 23, 24off 6279 . . . . . . 7
26 sibfof.3 . . . . . . . . . 10
27 sibfof.c . . . . . . . . . . 11
28 eqid 2404 . . . . . . . . . . 11
2927, 28tpsuni 16958 . . . . . . . . . 10
3026, 29syl 16 . . . . . . . . 9
31 eqid 2404 . . . . . . . . . . 11 sigaGen sigaGen
3231unieqi 3985 . . . . . . . . . 10 sigaGen sigaGen
33 fvex 5701 . . . . . . . . . . 11
34 unisg 24479 . . . . . . . . . . 11 sigaGen
3533, 34ax-mp 8 . . . . . . . . . 10 sigaGen
3632, 35eqtri 2424 . . . . . . . . 9 sigaGen
3730, 36syl6eqr 2454 . . . . . . . 8 sigaGen
38 feq3 5537 . . . . . . . 8 sigaGen sigaGen
3937, 38syl 16 . . . . . . 7 sigaGen
4025, 39mpbid 202 . . . . . 6 sigaGen
4133a1i 11 . . . . . . . . . 10
4241sgsiga 24478 . . . . . . . . 9 sigaGen sigAlgebra
4331, 42syl5eqel 2488 . . . . . . . 8 sigaGen sigAlgebra
44 uniexg 4665 . . . . . . . 8 sigaGen sigAlgebra sigaGen
4543, 44syl 16 . . . . . . 7 sigaGen
46 elmapg 6990 . . . . . . 7 sigaGen sigaGen sigaGen
4745, 23, 46syl2anc 643 . . . . . 6 sigaGen sigaGen
4840, 47mpbird 224 . . . . 5 sigaGen
49 inundif 3666 . . . . . . . . 9
5049imaeq2i 5160 . . . . . . . 8
51 ffun 5552 . . . . . . . . . 10
52 unpreima 5815 . . . . . . . . . 10
5325, 51, 523syl 19 . . . . . . . . 9
5453adantr 452 . . . . . . . 8 sigaGen
5550, 54syl5eqr 2450 . . . . . . 7 sigaGen
56 dmmeas 24508 . . . . . . . . . 10 measures sigAlgebra
5716, 56syl 16 . . . . . . . . 9 sigAlgebra
5857adantr 452 . . . . . . . 8 sigaGen sigAlgebra
59 imaiun 5951 . . . . . . . . . 10
60 iunid 4106 . . . . . . . . . . 11
6160imaeq2i 5160 . . . . . . . . . 10
6259, 61eqtr3i 2426 . . . . . . . . 9
63 inss2 3522 . . . . . . . . . . . 12
64 feq3 5537 . . . . . . . . . . . . . . . . . . . 20
656, 64syl 16 . . . . . . . . . . . . . . . . . . 19
6618, 65mpbird 224 . . . . . . . . . . . . . . . . . 18
67 feq3 5537 . . . . . . . . . . . . . . . . . . . 20
686, 67syl 16 . . . . . . . . . . . . . . . . . . 19
6920, 68mpbird 224 . . . . . . . . . . . . . . . . . 18
70 ffn 5550 . . . . . . . . . . . . . . . . . . 19
711, 70syl 16 . . . . . . . . . . . . . . . . . 18
7266, 69, 23, 71ofpreima 24034 . . . . . . . . . . . . . . . . 17
73 inundif 3666 . . . . . . . . . . . . . . . . . . 19
74 iuneq1 4066 . . . . . . . . . . . . . . . . . . 19
7573, 74ax-mp 8 . . . . . . . . . . . . . . . . . 18
76 iunxun 4132 . . . . . . . . . . . . . . . . . 18
7775, 76eqtr3i 2426 . . . . . . . . . . . . . . . . 17
7872, 77syl6eq 2452 . . . . . . . . . . . . . . . 16
79 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8079eldifbd 3293 . . . . . . . . . . . . . . . . . . . . . . . . 25
81 difssd 3435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
82 cnvimass 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
83 fdm 5554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
841, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8582, 84syl5sseq 3356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8681, 85sstrd 3318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8786sselda 3308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
88 1st2nd2 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
89 elxp6 6337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9089biimpri 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9190ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9287, 88, 913syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9392con3d 127 . . . . . . . . . . . . . . . . . . . . . . . . 25
9480, 93mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24
95 ianor 475 . . . . . . . . . . . . . . . . . . . . . . . 24
9694, 95sylib 189 . . . . . . . . . . . . . . . . . . . . . . 23
97 disjsn 3828 . . . . . . . . . . . . . . . . . . . . . . . 24
98 disjsn 3828 . . . . . . . . . . . . . . . . . . . . . . . 24
9997, 98orbi12i 508 . . . . . . . . . . . . . . . . . . . . . . 23
10096, 99sylibr 204 . . . . . . . . . . . . . . . . . . . . . 22
101 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10218, 101syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
103 dffn3 5557 . . . . . . . . . . . . . . . . . . . . . . . . 25
104102, 103sylib 189 . . . . . . . . . . . . . . . . . . . . . . . 24
105104adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
106 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10720, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
108 dffn3 5557 . . . . . . . . . . . . . . . . . . . . . . . . 25
109107, 108sylib 189 . . . . . . . . . . . . . . . . . . . . . . . 24
110109adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
111 fimacnvdisj 5580 . . . . . . . . . . . . . . . . . . . . . . . . . 26
112 ineq1 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
113 incom 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
114 in0 3613 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
115113, 114eqtri 2424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
116112, 115syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
117111, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
118117ex 424 . . . . . . . . . . . . . . . . . . . . . . . 24
119 fimacnvdisj 5580 . . . . . . . . . . . . . . . . . . . . . . . . . 26
120 ineq2 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
121 in0 3613 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
122120, 121syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123119, 122syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
124123ex 424 . . . . . . . . . . . . . . . . . . . . . . . 24
125118, 124jaao 496 . . . . . . . . . . . . . . . . . . . . . . 23
126105, 110, 125syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
127100, 126mpd 15 . . . . . . . . . . . . . . . . . . . . 21
128127ralrimiva 2749 . . . . . . . . . . . . . . . . . . . 20
129 iuneq2 4069 . . . . . . . . . . . . . . . . . . . 20
130128, 129syl 16 . . . . . . . . . . . . . . . . . . 19
131 iun0 4107 . . . . . . . . . . . . . . . . . . 19
132130, 131syl6eq 2452 . . . . . . . . . . . . . . . . . 18
133132uneq2d 3461 . . . . . . . . . . . . . . . . 17
134 un0 3612 . . . . . . . . . . . . . . . . 17
135133, 134syl6eq 2452 . . . . . . . . . . . . . . . 16
13678, 135eqtrd 2436 . . . . . . . . . . . . . . 15
137136adantr 452 . . . . . . . . . . . . . 14
13857adantr 452 . . . . . . . . . . . . . . 15 sigAlgebra
13957ad2antrr 707 . . . . . . . . . . . . . . . . 17 sigAlgebra
140 simpll 731 . . . . . . . . . . . . . . . . . 18
141 inss1 3521 . . . . . . . . . . . . . . . . . . . 20
14285adantr 452 . . . . . . . . . . . . . . . . . . . 20
143141, 142syl5ss 3319 . . . . . . . . . . . . . . . . . . 19
144143sselda 3308 . . . . . . . . . . . . . . . . . 18
14557adantr 452 . . . . . . . . . . . . . . . . . . 19 sigAlgebra
146 fvex 5701 . . . . . . . . . . . . . . . . . . . . . . . 24
1474, 146eqeltri 2474 . . . . . . . . . . . . . . . . . . . . . . 23
148147a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
149148sgsiga 24478 . . . . . . . . . . . . . . . . . . . . 21 sigaGen sigAlgebra
15011, 149syl5eqel 2488 . . . . . . . . . . . . . . . . . . . 20 sigAlgebra
151150adantr 452 . . . . . . . . . . . . . . . . . . 19 sigAlgebra
1523, 4, 11, 12, 13, 14, 15, 16, 17sibfmbl 24603 . . . . . . . . . . . . . . . . . . . 20 MblFnM
153152adantr 452 . . . . . . . . . . . . . . . . . . 19 MblFnM
1544tpstop 16959 . . . . . . . . . . . . . . . . . . . . . . 23
155 cldssbrsiga 24494 . . . . . . . . . . . . . . . . . . . . . . 23 sigaGen
1562, 154, 1553syl 19 . . . . . . . . . . . . . . . . . . . . . 22 sigaGen
157156adantr 452 . . . . . . . . . . . . . . . . . . . . 21 sigaGen
158 sibfof.4 . . . . . . . . . . . . . . . . . . . . . . 23
159158adantr 452 . . . . . . . . . . . . . . . . . . . . . 22
160 xp1st 6335 . . . . . . . . . . . . . . . . . . . . . . . 24
161160adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
1626adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
163161, 162eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . 22
164 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . 23
165164t1sncld 17344 . . . . . . . . . . . . . . . . . . . . . 22
166159, 163, 165syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
167157, 166sseldd 3309 . . . . . . . . . . . . . . . . . . . 20 sigaGen
168167, 11syl6eleqr 2495 . . . . . . . . . . . . . . . . . . 19
169145, 151, 153, 168mbfmcnvima 24560 . . . . . . . . . . . . . . . . . 18
170140, 144, 169syl2anc 643 . . . . . . . . . . . . . . . . 17
1713, 4, 11, 12, 13, 14, 15, 16, 19sibfmbl 24603 . . . . . . . . . . . . . . . . . . . 20 MblFnM
172171adantr 452 . . . . . . . . . . . . . . . . . . 19 MblFnM
173 xp2nd 6336 . . . . . . . . . . . . . . . . . . . . . . . 24
174173adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
175174, 162eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . 22
176164t1sncld 17344 . . . . . . . . . . . . . . . . . . . . . 22
177159, 175, 176syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
178157, 177sseldd 3309 . . . . . . . . . . . . . . . . . . . 20 sigaGen
179178, 11syl6eleqr 2495 . . . . . . . . . . . . . . . . . . 19
180145, 151, 172, 179mbfmcnvima 24560 . . . . . . . . . . . . . . . . . 18
181140, 144, 180syl2anc 643 . . . . . . . . . . . . . . . . 17
182 inelsiga 24471 . . . . . . . . . . . . . . . . 17 sigAlgebra
183139, 170, 181, 182syl3anc 1184 . . . . . . . . . . . . . . . 16
184183ralrimiva 2749 . . . . . . . . . . . . . . 15
185 inss2 3522 . . . . . . . . . . . . . . . . . 18
1863, 4, 11, 12, 13, 14, 15, 16, 17sibfrn 24605 . . . . . . . . . . . . . . . . . . . 20
1873, 4, 11, 12, 13, 14, 15, 16, 19sibfrn 24605 . . . . . . . . . . . . . . . . . . . 20
188 xpfi 7337 . . . . . . . . . . . . . . . . . . . 20
189186, 187, 188syl2anc 643 . . . . . . . . . . . . . . . . . . 19
190 ssdomg 7112 . . . . . . . . . . . . . . . . . . 19
191189, 190syl 16 . . . . . . . . . . . . . . . . . 18
192185, 191mpi 17 . . . . . . . . . . . . . . . . 17
193 isfinite 7563 . . . . . . . . . . . . . . . . . . 19
194193biimpi 187 . . . . . . . . . . . . . . . . . 18
195 sdomdom 7094 . . . . . . . . . . . . . . . . . 18
196189, 194, 1953syl 19 . . . . . . . . . . . . . . . . 17
197 domtr 7119 . . . . . . . . . . . . . . . . 17
198192, 196, 197syl2anc 643 . . . . . . . . . . . . . . . 16
199198adantr 452 . . . . . . . . . . . . . . 15
200 nfcv 2540 . . . . . . . . . . . . . . . 16
201200sigaclcuni 24454 . . . . . . . . . . . . . . 15 sigAlgebra
202138, 184, 199, 201syl3anc 1184 . . . . . . . . . . . . . 14
203137, 202eqeltrd 2478 . . . . . . . . . . . . 13
204203ralrimiva 2749 . . . . . . . . . . . 12
205 ssralv 3367 . . . . . . . . . . . 12
20663, 204, 205mpsyl 61 . . . . . . . . . . 11
207206adantr 452 . . . . . . . . . 10 sigaGen
208 ffun 5552 . . . . . . . . . . . . . . . . 17
2091, 208syl 16 . . . . . . . . . . . . . . . 16
210 imafi 7357 . . . . . . . . . . . . . . . 16
211209, 189, 210syl2anc 643 . . . . . . . . . . . . . . 15
21218, 20, 9, 23ofrn2 24006 . . . . . . . . . . . . . . 15
213 ssfi 7288 . . . . . . . . . . . . . . 15
214211, 212, 213syl2anc 643 . . . . . . . . . . . . . 14
215 ssdomg 7112 . . . . . . . . . . . . . 14
216214, 215syl 16 . . . . . . . . . . . . 13
21763, 216mpi 17 . . . . . . . . . . . 12
218 isfinite 7563 . . . . . . . . . . . . . 14
219214, 218sylib 189 . . . . . . . . . . . . 13
220 sdomdom 7094 . . . . . . . . . . . . 13
221219, 220syl 16 . . . . . . . . . . . 12
222 domtr 7119 . . . . . . . . . . . 12
223217, 221, 222syl2anc 643 . . . . . . . . . . 11
224223adantr 452 . . . . . . . . . 10 sigaGen
225 nfcv 2540 . . . . . . . . . . 11
226225sigaclcuni 24454 . . . . . . . . . 10 sigAlgebra
22758, 207, 224, 226syl3anc 1184 . . . . . . . . 9 sigaGen
22862, 227syl5eqelr 2489 . . . . . . . 8 sigaGen
229 difpreima 5817 . . . . . . . . . . . 12
23025, 51, 2293syl 19 . . . . . . . . . . 11
231 cnvimarndm 5184 . . . . . . . . . . . . 13
232231difeq2i 3422 . . . . . . . . . . . 12
233 cnvimass 5183 . . . . . . . . . . . . 13
234 ssdif0 3646 . . . . . . . . . . . . 13
235233, 234mpbi 200 . . . . . . . . . . . 12
236232, 235eqtri 2424 . . . . . . . . . . 11
237230, 236syl6eq 2452 . . . . . . . . . 10
238 0elsiga 24450 . . . . . . . . . . 11 sigAlgebra
23957, 238syl 16 . . . . . . . . . 10
240237, 239eqeltrd 2478 . . . . . . . . 9
241240adantr 452 . . . . . . . 8 sigaGen
242 unelsiga 24470 . . . . . . . 8 sigAlgebra
24358, 228, 241, 242syl3anc 1184 . . . . . . 7 sigaGen
24455, 243eqeltrd 2478 . . . . . 6 sigaGen
245244ralrimiva 2749 . . . . 5 sigaGen
24648, 245jca 519 . . . 4 sigaGen sigaGen
24757, 43ismbfm 24555 . . . 4 MblFnMsigaGen sigaGen sigaGen
248246, 247mpbird 224 . . 3 MblFnMsigaGen
249136adantr 452 . . . . . . . 8
250249fveq2d 5691 . . . . . . 7
251 measbasedom 24509 . . . . . . . . . 10 measures measures
25216, 251sylib 189 . . . . . . . . 9 measures
253252adantr 452 . . . . . . . 8 measures
254 difss 3434 . . . . . . . . . 10
255254sseli 3304 . . . . . . . . 9
256255, 184sylan2 461 . . . . . . . 8
257198adantr 452 . . . . . . . . 9
258 ffun 5552 . . . . . . . . . . . . . 14
25918, 258syl 16 . . . . . . . . . . . . 13
260 sndisj 4164 . . . . . . . . . . . . 13 Disj
261 disjpreima 23979 . . . . . . . . . . . . 13 Disj Disj
262259, 260, 261sylancl 644 . . . . . . . . . . . 12 Disj
263 ffun 5552 . . . . . . . . . . . . . 14
26420, 263syl 16 . . . . . . . . . . . . 13
265 sndisj 4164 . . . . . . . . . . . . 13 Disj
266 disjpreima 23979 . . . . . . . . . . . . 13 Disj Disj
267264, 265, 266sylancl 644 . . . . . . . . . . . 12 Disj
268 sneq 3785 . . . . . . . . . . . . . 14
269268imaeq2d 5162 . . . . . . . . . . . . 13
270 sneq 3785 . . . . . . . . . . . . . 14
271270imaeq2d 5162 . . . . . . . . . . . . 13
272 simpl 444 . . . . . . . . . . . . 13 Disj Disj Disj
273 simpr 448 . . . . . . . . . . . . 13 Disj Disj Disj
274269, 271, 272, 273disjxpin 23981 . . . . . . . . . . . 12 Disj Disj Disj
275262, 267, 274syl2anc 643 . . . . . . . . . . 11 Disj
276 disjss1 4148 . . . . . . . . . . 11 Disj Disj
277185, 275, 276mpsyl 61 . . . . . . . . . 10 Disj
278277adantr 452 . . . . . . . . 9 Disj
279257, 278jca 519 . . . . . . . 8 Disj
280 measvuni 24521 . . . . . . . 8 measures Disj Σ*
281253, 256, 279, 280syl3anc 1184 . . . . . . 7 Σ*
282 ssfi 7288 . . . . . . . . . 10
283189, 185, 282sylancl 644 . . . . . . . . 9
284283adantr 452 . . . . . . . 8
285 iccssxr 10949 . . . . . . . . . . 11
286253adantr 452 . . . . . . . . . . . 12 measures
287255, 183sylanl2 633 . . . . . . . . . . . 12
288 measvxrge0 24512 . . . . . . . . . . . 12 measures
289286, 287, 288syl2anc 643 . . . . . . . . . . 11
290285, 289sseldi 3306 . . . . . . . . . 10
291 measge0 24514 . . . . . . . . . . 11 measures
292286, 287, 291syl2anc 643 . . . . . . . . . 10
293 simpl 444 . . . . . . . . . . 11
294 simpr 448 . . . . . . . . . . 11
295255, 140sylanl2 633 . . . . . . . . . . . 12
296185, 294sseldi 3306 . . . . . . . . . . . . . . . . . 18
297 xp1st 6335 . . . . . . . . . . . . . . . . . 18
298296, 297syl 16 . . . . . . . . . . . . . . . . 17
299298orcd 382 . . . . . . . . . . . . . . . 16
300298orcd 382 . . . . . . . . . . . . . . . 16
301299, 300jca 519 . . . . . . . . . . . . . . 15
302 xp2nd 6336 . . . . . . . . . . . . . . . . . 18
303296, 302syl 16 . . . . . . . . . . . . . . . . 17
304303olcd 383 . . . . . . . . . . . . . . . 16
305 oveq12 6049 . . . . . . . . . . . . . . . . . . . . . . . . . 26
306305adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25
307 sibfof.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26
308307adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
309306, 308eqtrd 2436 . . . . . . . . . . . . . . . . . . . . . . . 24
310309ex 424 . . . . . . . . . . . . . . . . . . . . . . 23
311310necon3ad 2603 . . . . . . . . . . . . . . . . . . . . . 22
312 oran 483 . . . . . . . . . . . . . . . . . . . . . . 23
313 nne 2571 . . . . . . . . . . . . . . . . . . . . . . . . 25
314 nne 2571 . . . . . . . . . . . . . . . . . . . . . . . . 25
315313, 314anbi12i 679 . . . . . . . . . . . . . . . . . . . . . . . 24
316315notbii 288 . . . . . . . . . . . . . . . . . . . . . . 23
317312, 316bitri 241 . . . . . . . . . . . . . . . . . . . . . 22
318311, 317syl6ibr 219 . . . . . . . . . . . . . . . . . . . . 21
319318adantr 452 . . . . . . . . . . . . . . . . . . . 20
320319ralrimivva 2758 . . . . . . . . . . . . . . . . . . 19
321295, 320syl 16 . . . . . . . . . . . . . . . . . 18
322141a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
323322sselda 3308 . . . . . . . . . . . . . . . . . . . . 21
324295, 71syl 16 . . . . . . . . . . . . . . . . . . . . . 22
325 fniniseg 5810 . . . . . . . . . . . . . . . . . . . . . 22
326324, 325syl 16 . . . . . . . . . . . . . . . . . . . . 21
327323, 326mpbid 202 . . . . . . . . . . . . . . . . . . . 20
328 simpr 448 . . . . . . . . . . . . . . . . . . . . 21
32988fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . 23
330 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . . 23
331329, 330syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . 22
332331adantr 452 . . . . . . . . . . . . . . . . . . . . 21
333328, 332eqtr3d 2438 . . . . . . . . . . . . . . . . . . . 20
334327, 333syl 16 . . . . . . . . . . . . . . . . . . 19
335 simplr 732 . . . . . . . . . . . . . . . . . . . . 21
336335eldifbd 3293 . . . . . . . . . . . . . . . . . . . 20
337 elsn 3789 . . . . . . . . . . . . . . . . . . . . 21
338337necon3bbii 2598 . . . . . . . . . . . . . . . . . . . 20
339336, 338sylib 189 . . . . . . . . . . . . . . . . . . 19
340334, 339eqnetrrd 2587 . . . . . . . . . . . . . . . . . 18
341255, 144sylanl2 633 . . . . . . . . . . . . . . . . . . . 20
342341, 160syl 16 . . . . . . . . . . . . . . . . . . 19
343341, 173syl 16 . . . . . . . . . . . . . . . . . . 19
344 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . 22
345344neeq1d 2580 . . . . . . . . . . . . . . . . . . . . 21
346 neeq1 2575 . . . . . . . . . . . . . . . . . . . . . 22
347346orbi1d 684 . . . . . . . . . . . . . . . . . . . . 21
348345, 347imbi12d 312 . . . . . . . . . . . . . . . . . . . 20
349 oveq2 6048 . . . . . . . . . . . . . . . . . . . . . 22
350349neeq1d 2580 . . . . . . . . . . . . . . . . . . . . 21
351 neeq1 2575 . . . . . . . . . . . . . . . . . . . . . 22
352351orbi2d 683 . . . . . . . . . . . . . . . . . . . . 21
353350, 352imbi12d 312 . . . . . . . . . . . . . . . . . . . 20
354348, 353rspc2v 3018 . . . . . . . . . . . . . . . . . . 19
355342, 343, 354syl2anc 643 . . . . . . . . . . . . . . . . . 18
356321, 340, 355mp2d 43 . . . . . . . . . . . . . . . . 17
357 fvex 5701 . . . . . . . . . . . . . . . . . . . 20
358357elsnc 3797 . . . . . . . . . . . . . . . . . . 19
359358necon3bbii 2598 . . . . . . . . . . . . . . . . . 18
360 fvex 5701 . . . . . . . . . . . . . . . . . . . 20
361360elsnc 3797 . . . . . . . . . . . . . . . . . . 19
362361necon3bbii 2598 . . . . . . . . . . . . . . . . . 18
363359, 362orbi12i 508 . . . . . . . . . . . . . . . . 17
364356, 363sylibr 204 . . . . . . . . . . . . . . . 16
365304, 364jca 519 . . . . . . . . . . . . . . 15
366301, 365jca 519 . . . . . . . . . . . . . 14
367 orddi 840 . . . . . . . . . . . . . 14
368366, 367sylibr 204 . . . . . . . . . . . . 13
369 eldif 3290 . . . . . . . . . . . . . 14
370 eldif 3290 . . . . . . . . . . . . . 14
371369, 370orbi12i 508 . . . . . . . . . . . . 13
372368, 371sylibr 204 . . . . . . . . . . . 12
3733, 4, 11, 12, 13, 14, 15, 16, 17sibfima 24606 . . . . . . . . . . . . . . 15
374 0re 9047 . . . . . . . . . . . . . . . . . 18
375 pnfxr 10669 . . . . . . . . . . . . . . . . . 18
376 elico2 10930 . . . . . . . . . . . . . . . . . 18