Metamath Proof Explorer

Theorem ovoliunnul

Description: A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015)

Ref Expression
Assertion ovoliunnul 
|- ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( vol* ` U_ n e. A B ) = 0 )

Proof

Step Hyp Ref Expression
1 iuneq1 
 |-  ( A = (/) -> U_ n e. A B = U_ n e. (/) B )
2 0iun 
 |-  U_ n e. (/) B = (/)
3 1 2 eqtrdi 
 |-  ( A = (/) -> U_ n e. A B = (/) )
4 3 fveq2d 
 |-  ( A = (/) -> ( vol* ` U_ n e. A B ) = ( vol* ` (/) ) )
5 ovol0 
 |-  ( vol* ` (/) ) = 0
6 4 5 eqtrdi 
 |-  ( A = (/) -> ( vol* ` U_ n e. A B ) = 0 )
7 6 a1i 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( A = (/) -> ( vol* ` U_ n e. A B ) = 0 ) )
8 reldom 
 |-  Rel ~<_
9 8 brrelex1i 
 |-  ( A ~<_ NN -> A e. _V )
10 9 adantr 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> A e. _V )
11 0sdomg 
 |-  ( A e. _V -> ( (/) ~< A <-> A =/= (/) ) )
12 10 11 syl 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( (/) ~< A <-> A =/= (/) ) )
13 fodomr 
 |-  ( ( (/) ~< A /\ A ~<_ NN ) -> E. f f : NN -onto-> A )
14 13 expcom 
 |-  ( A ~<_ NN -> ( (/) ~< A -> E. f f : NN -onto-> A ) )
15 14 adantr 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( (/) ~< A -> E. f f : NN -onto-> A ) )
16 eliun 
 |-  ( x e. U_ n e. A B <-> E. n e. A x e. B )
17 nfv 
 |-  F/ n f : NN -onto-> A
18 nfcv 
 |-  F/_ n NN
19 nfcsb1v 
 |-  F/_ n [_ ( f ` k ) / n ]_ B
20 18 19 nfiun 
 |-  F/_ n U_ k e. NN [_ ( f ` k ) / n ]_ B
21 20 nfcri 
 |-  F/ n x e. U_ k e. NN [_ ( f ` k ) / n ]_ B
22 foelrn 
 |-  ( ( f : NN -onto-> A /\ n e. A ) -> E. k e. NN n = ( f ` k ) )
23 22 ex 
 |-  ( f : NN -onto-> A -> ( n e. A -> E. k e. NN n = ( f ` k ) ) )
24 csbeq1a 
 |-  ( n = ( f ` k ) -> B = [_ ( f ` k ) / n ]_ B )
25 24 adantl 
 |-  ( ( f : NN -onto-> A /\ n = ( f ` k ) ) -> B = [_ ( f ` k ) / n ]_ B )
26 25 eleq2d 
 |-  ( ( f : NN -onto-> A /\ n = ( f ` k ) ) -> ( x e. B <-> x e. [_ ( f ` k ) / n ]_ B ) )
27 26 biimpd 
 |-  ( ( f : NN -onto-> A /\ n = ( f ` k ) ) -> ( x e. B -> x e. [_ ( f ` k ) / n ]_ B ) )
28 27 impancom 
 |-  ( ( f : NN -onto-> A /\ x e. B ) -> ( n = ( f ` k ) -> x e. [_ ( f ` k ) / n ]_ B ) )
29 28 reximdv 
 |-  ( ( f : NN -onto-> A /\ x e. B ) -> ( E. k e. NN n = ( f ` k ) -> E. k e. NN x e. [_ ( f ` k ) / n ]_ B ) )
30 eliun 
 |-  ( x e. U_ k e. NN [_ ( f ` k ) / n ]_ B <-> E. k e. NN x e. [_ ( f ` k ) / n ]_ B )
31 29 30 imbitrrdi 
 |-  ( ( f : NN -onto-> A /\ x e. B ) -> ( E. k e. NN n = ( f ` k ) -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) )
32 31 ex 
 |-  ( f : NN -onto-> A -> ( x e. B -> ( E. k e. NN n = ( f ` k ) -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) )
33 32 com23 
 |-  ( f : NN -onto-> A -> ( E. k e. NN n = ( f ` k ) -> ( x e. B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) )
34 23 33 syld 
 |-  ( f : NN -onto-> A -> ( n e. A -> ( x e. B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) )
35 17 21 34 rexlimd 
 |-  ( f : NN -onto-> A -> ( E. n e. A x e. B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) )
36 16 35 biimtrid 
 |-  ( f : NN -onto-> A -> ( x e. U_ n e. A B -> x e. U_ k e. NN [_ ( f ` k ) / n ]_ B ) )
37 36 ssrdv 
 |-  ( f : NN -onto-> A -> U_ n e. A B C_ U_ k e. NN [_ ( f ` k ) / n ]_ B )
38 37 adantl 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> U_ n e. A B C_ U_ k e. NN [_ ( f ` k ) / n ]_ B )
39 fof 
 |-  ( f : NN -onto-> A -> f : NN --> A )
40 39 adantl 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> f : NN --> A )
41 40 ffvelcdmda 
 |-  ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( f ` k ) e. A )
42 simpllr 
 |-  ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) )
43 nfcv 
 |-  F/_ n RR
44 19 43 nfss 
 |-  F/ n [_ ( f ` k ) / n ]_ B C_ RR
45 nfcv 
 |-  F/_ n vol*
46 45 19 nffv 
 |-  F/_ n ( vol* ` [_ ( f ` k ) / n ]_ B )
47 46 nfeq1 
 |-  F/ n ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0
48 44 47 nfan 
 |-  F/ n ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 )
49 24 sseq1d 
 |-  ( n = ( f ` k ) -> ( B C_ RR <-> [_ ( f ` k ) / n ]_ B C_ RR ) )
50 24 fveqeq2d 
 |-  ( n = ( f ` k ) -> ( ( vol* ` B ) = 0 <-> ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) )
51 49 50 anbi12d 
 |-  ( n = ( f ` k ) -> ( ( B C_ RR /\ ( vol* ` B ) = 0 ) <-> ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) ) )
52 48 51 rspc 
 |-  ( ( f ` k ) e. A -> ( A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) -> ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) ) )
53 41 42 52 sylc 
 |-  ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 ) )
54 53 simpld 
 |-  ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> [_ ( f ` k ) / n ]_ B C_ RR )
55 54 ralrimiva 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> A. k e. NN [_ ( f ` k ) / n ]_ B C_ RR )
56 iunss 
 |-  ( U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR <-> A. k e. NN [_ ( f ` k ) / n ]_ B C_ RR )
57 55 56 sylibr 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR )
58 eqid 
 |-  seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) = seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) )
59 eqid 
 |-  ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) = ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) )
60 53 simprd 
 |-  ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 )
61 0re 
 |-  0 e. RR
62 60 61 eqeltrdi 
 |-  ( ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) /\ k e. NN ) -> ( vol* ` [_ ( f ` k ) / n ]_ B ) e. RR )
63 60 mpteq2dva 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) = ( k e. NN |-> 0 ) )
64 fconstmpt 
 |-  ( NN X. { 0 } ) = ( k e. NN |-> 0 )
65 nnuz 
 |-  NN = ( ZZ>= ` 1 )
66 65 xpeq1i 
 |-  ( NN X. { 0 } ) = ( ( ZZ>= ` 1 ) X. { 0 } )
67 64 66 eqtr3i 
 |-  ( k e. NN |-> 0 ) = ( ( ZZ>= ` 1 ) X. { 0 } )
68 63 67 eqtrdi 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) = ( ( ZZ>= ` 1 ) X. { 0 } ) )
69 68 seqeq3d 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) = seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) )
70 1z 
 |-  1 e. ZZ
71 serclim0 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 )
72 seqex 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) e. _V
73 c0ex 
 |-  0 e. _V
74 72 73 breldm 
 |-  ( seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) e. dom ~~> )
75 70 71 74 mp2b 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) e. dom ~~>
76 69 75 eqeltrdi 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> seq 1 ( + , ( k e. NN |-> ( vol* ` [_ ( f ` k ) / n ]_ B ) ) ) e. dom ~~> )
77 58 59 54 62 76 ovoliun2 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ sum_ k e. NN ( vol* ` [_ ( f ` k ) / n ]_ B ) )
78 60 sumeq2dv 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> sum_ k e. NN ( vol* ` [_ ( f ` k ) / n ]_ B ) = sum_ k e. NN 0 )
79 65 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
80 79 orci 
 |-  ( NN C_ ( ZZ>= ` 1 ) \/ NN e. Fin )
81 sumz 
 |-  ( ( NN C_ ( ZZ>= ` 1 ) \/ NN e. Fin ) -> sum_ k e. NN 0 = 0 )
82 80 81 ax-mp 
 |-  sum_ k e. NN 0 = 0
83 78 82 eqtrdi 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> sum_ k e. NN ( vol* ` [_ ( f ` k ) / n ]_ B ) = 0 )
84 77 83 breqtrd 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ 0 )
85 ovolge0 
 |-  ( U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR -> 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) )
86 57 85 syl 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) )
87 ovolcl 
 |-  ( U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) e. RR* )
88 57 87 syl 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) e. RR* )
89 0xr 
 |-  0 e. RR*
90 xrletri3 
 |-  ( ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) e. RR* /\ 0 e. RR* ) -> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 <-> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ 0 /\ 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) )
91 88 89 90 sylancl 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 <-> ( ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) <_ 0 /\ 0 <_ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) ) ) )
92 84 86 91 mpbir2and 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 )
93 ovolssnul 
 |-  ( ( U_ n e. A B C_ U_ k e. NN [_ ( f ` k ) / n ]_ B /\ U_ k e. NN [_ ( f ` k ) / n ]_ B C_ RR /\ ( vol* ` U_ k e. NN [_ ( f ` k ) / n ]_ B ) = 0 ) -> ( vol* ` U_ n e. A B ) = 0 )
94 38 57 92 93 syl3anc 
 |-  ( ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) /\ f : NN -onto-> A ) -> ( vol* ` U_ n e. A B ) = 0 )
95 94 ex 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( f : NN -onto-> A -> ( vol* ` U_ n e. A B ) = 0 ) )
96 95 exlimdv 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( E. f f : NN -onto-> A -> ( vol* ` U_ n e. A B ) = 0 ) )
97 15 96 syld 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( (/) ~< A -> ( vol* ` U_ n e. A B ) = 0 ) )
98 12 97 sylbird 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( A =/= (/) -> ( vol* ` U_ n e. A B ) = 0 ) )
99 7 98 pm2.61dne 
 |-  ( ( A ~<_ NN /\ A. n e. A ( B C_ RR /\ ( vol* ` B ) = 0 ) ) -> ( vol* ` U_ n e. A B ) = 0 )