This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovoliun

Description: The Lebesgue outer measure function is countably sub-additive. (Many books allow +oo as a value for one of the sets in the sum, but in our setup we can't do arithmetic on infinity, and in any case the volume of a union containing an infinitely large set is already infinitely large by monotonicity ovolss , so we need not consider this case here, although we do allow the sum itself to be infinite.) (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t 
|- T = seq 1 ( + , G )
ovoliun.g 
|- G = ( n e. NN |-> ( vol* ` A ) )
ovoliun.a 
|- ( ( ph /\ n e. NN ) -> A C_ RR )
ovoliun.v 
|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
Assertion ovoliun 
|- ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t 
 |-  T = seq 1 ( + , G )
2 ovoliun.g 
 |-  G = ( n e. NN |-> ( vol* ` A ) )
3 ovoliun.a 
 |-  ( ( ph /\ n e. NN ) -> A C_ RR )
4 ovoliun.v 
 |-  ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
5 mnfxr 
 |-  -oo e. RR*
6 5 a1i 
 |-  ( ph -> -oo e. RR* )
7 nnuz 
 |-  NN = ( ZZ>= ` 1 )
8 1zzd 
 |-  ( ph -> 1 e. ZZ )
9 4 2 fmptd 
 |-  ( ph -> G : NN --> RR )
10 9 ffvelcdmda 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )
11 7 8 10 serfre 
 |-  ( ph -> seq 1 ( + , G ) : NN --> RR )
12 1 feq1i 
 |-  ( T : NN --> RR <-> seq 1 ( + , G ) : NN --> RR )
13 11 12 sylibr 
 |-  ( ph -> T : NN --> RR )
14 1nn 
 |-  1 e. NN
15 ffvelcdm 
 |-  ( ( T : NN --> RR /\ 1 e. NN ) -> ( T ` 1 ) e. RR )
16 13 14 15 sylancl 
 |-  ( ph -> ( T ` 1 ) e. RR )
17 16 rexrd 
 |-  ( ph -> ( T ` 1 ) e. RR* )
18 13 frnd 
 |-  ( ph -> ran T C_ RR )
19 ressxr 
 |-  RR C_ RR*
20 18 19 sstrdi 
 |-  ( ph -> ran T C_ RR* )
21 supxrcl 
 |-  ( ran T C_ RR* -> sup ( ran T , RR* , < ) e. RR* )
22 20 21 syl 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR* )
23 16 mnfltd 
 |-  ( ph -> -oo < ( T ` 1 ) )
24 13 ffnd 
 |-  ( ph -> T Fn NN )
25 fnfvelrn 
 |-  ( ( T Fn NN /\ 1 e. NN ) -> ( T ` 1 ) e. ran T )
26 24 14 25 sylancl 
 |-  ( ph -> ( T ` 1 ) e. ran T )
27 supxrub 
 |-  ( ( ran T C_ RR* /\ ( T ` 1 ) e. ran T ) -> ( T ` 1 ) <_ sup ( ran T , RR* , < ) )
28 20 26 27 syl2anc 
 |-  ( ph -> ( T ` 1 ) <_ sup ( ran T , RR* , < ) )
29 6 17 22 23 28 xrltletrd 
 |-  ( ph -> -oo < sup ( ran T , RR* , < ) )
30 xrrebnd 
 |-  ( sup ( ran T , RR* , < ) e. RR* -> ( sup ( ran T , RR* , < ) e. RR <-> ( -oo < sup ( ran T , RR* , < ) /\ sup ( ran T , RR* , < ) < +oo ) ) )
31 22 30 syl 
 |-  ( ph -> ( sup ( ran T , RR* , < ) e. RR <-> ( -oo < sup ( ran T , RR* , < ) /\ sup ( ran T , RR* , < ) < +oo ) ) )
32 29 31 mpbirand 
 |-  ( ph -> ( sup ( ran T , RR* , < ) e. RR <-> sup ( ran T , RR* , < ) < +oo ) )
33 nfcv 
 |-  F/_ m A
34 nfcsb1v 
 |-  F/_ n [_ m / n ]_ A
35 csbeq1a 
 |-  ( n = m -> A = [_ m / n ]_ A )
36 33 34 35 cbviun 
 |-  U_ n e. NN A = U_ m e. NN [_ m / n ]_ A
37 36 fveq2i 
 |-  ( vol* ` U_ n e. NN A ) = ( vol* ` U_ m e. NN [_ m / n ]_ A )
38 nfcv 
 |-  F/_ m ( vol* ` A )
39 nfcv 
 |-  F/_ n vol*
40 39 34 nffv 
 |-  F/_ n ( vol* ` [_ m / n ]_ A )
41 35 fveq2d 
 |-  ( n = m -> ( vol* ` A ) = ( vol* ` [_ m / n ]_ A ) )
42 38 40 41 cbvmpt 
 |-  ( n e. NN |-> ( vol* ` A ) ) = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
43 2 42 eqtri 
 |-  G = ( m e. NN |-> ( vol* ` [_ m / n ]_ A ) )
44 3 ralrimiva 
 |-  ( ph -> A. n e. NN A C_ RR )
45 nfv 
 |-  F/ m A C_ RR
46 nfcv 
 |-  F/_ n RR
47 34 46 nfss 
 |-  F/ n [_ m / n ]_ A C_ RR
48 35 sseq1d 
 |-  ( n = m -> ( A C_ RR <-> [_ m / n ]_ A C_ RR ) )
49 45 47 48 cbvralw 
 |-  ( A. n e. NN A C_ RR <-> A. m e. NN [_ m / n ]_ A C_ RR )
50 44 49 sylib 
 |-  ( ph -> A. m e. NN [_ m / n ]_ A C_ RR )
51 50 ad2antrr 
 |-  ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> A. m e. NN [_ m / n ]_ A C_ RR )
52 51 r19.21bi 
 |-  ( ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) /\ m e. NN ) -> [_ m / n ]_ A C_ RR )
53 4 ralrimiva 
 |-  ( ph -> A. n e. NN ( vol* ` A ) e. RR )
54 38 nfel1 
 |-  F/ m ( vol* ` A ) e. RR
55 40 nfel1 
 |-  F/ n ( vol* ` [_ m / n ]_ A ) e. RR
56 41 eleq1d 
 |-  ( n = m -> ( ( vol* ` A ) e. RR <-> ( vol* ` [_ m / n ]_ A ) e. RR ) )
57 54 55 56 cbvralw 
 |-  ( A. n e. NN ( vol* ` A ) e. RR <-> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
58 53 57 sylib 
 |-  ( ph -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
59 58 ad2antrr 
 |-  ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> A. m e. NN ( vol* ` [_ m / n ]_ A ) e. RR )
60 59 r19.21bi 
 |-  ( ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) /\ m e. NN ) -> ( vol* ` [_ m / n ]_ A ) e. RR )
61 simplr 
 |-  ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> sup ( ran T , RR* , < ) e. RR )
62 simpr 
 |-  ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> x e. RR+ )
63 1 43 52 60 61 62 ovoliunlem3 
 |-  ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> ( vol* ` U_ m e. NN [_ m / n ]_ A ) <_ ( sup ( ran T , RR* , < ) + x ) )
64 37 63 eqbrtrid 
 |-  ( ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) /\ x e. RR+ ) -> ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) )
65 64 ralrimiva 
 |-  ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) -> A. x e. RR+ ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) )
66 iunss 
 |-  ( U_ n e. NN A C_ RR <-> A. n e. NN A C_ RR )
67 44 66 sylibr 
 |-  ( ph -> U_ n e. NN A C_ RR )
68 ovolcl 
 |-  ( U_ n e. NN A C_ RR -> ( vol* ` U_ n e. NN A ) e. RR* )
69 67 68 syl 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) e. RR* )
70 xralrple 
 |-  ( ( ( vol* ` U_ n e. NN A ) e. RR* /\ sup ( ran T , RR* , < ) e. RR ) -> ( ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) <-> A. x e. RR+ ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) ) )
71 69 70 sylan 
 |-  ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) -> ( ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) <-> A. x e. RR+ ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + x ) ) )
72 65 71 mpbird 
 |-  ( ( ph /\ sup ( ran T , RR* , < ) e. RR ) -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )
73 72 ex 
 |-  ( ph -> ( sup ( ran T , RR* , < ) e. RR -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
74 32 73 sylbird 
 |-  ( ph -> ( sup ( ran T , RR* , < ) < +oo -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
75 nltpnft 
 |-  ( sup ( ran T , RR* , < ) e. RR* -> ( sup ( ran T , RR* , < ) = +oo <-> -. sup ( ran T , RR* , < ) < +oo ) )
76 22 75 syl 
 |-  ( ph -> ( sup ( ran T , RR* , < ) = +oo <-> -. sup ( ran T , RR* , < ) < +oo ) )
77 pnfge 
 |-  ( ( vol* ` U_ n e. NN A ) e. RR* -> ( vol* ` U_ n e. NN A ) <_ +oo )
78 69 77 syl 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ +oo )
79 breq2 
 |-  ( sup ( ran T , RR* , < ) = +oo -> ( ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) <-> ( vol* ` U_ n e. NN A ) <_ +oo ) )
80 78 79 syl5ibrcom 
 |-  ( ph -> ( sup ( ran T , RR* , < ) = +oo -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
81 76 80 sylbird 
 |-  ( ph -> ( -. sup ( ran T , RR* , < ) < +oo -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) ) )
82 74 81 pm2.61d 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran T , RR* , < ) )