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 syl6ibr
 |-  ( ( 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 syl5bi
 |-  ( 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 ffvelrnda
 |-  ( ( ( ( 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 )