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 𝑇 = seq 1 ( + , 𝐺 )
ovoliun.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
ovoliun.a ( ( 𝜑𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
ovoliun.v ( ( 𝜑𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
Assertion ovoliun ( 𝜑 → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t 𝑇 = seq 1 ( + , 𝐺 )
2 ovoliun.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) )
3 ovoliun.a ( ( 𝜑𝑛 ∈ ℕ ) → 𝐴 ⊆ ℝ )
4 ovoliun.v ( ( 𝜑𝑛 ∈ ℕ ) → ( vol* ‘ 𝐴 ) ∈ ℝ )
5 mnfxr -∞ ∈ ℝ*
6 5 a1i ( 𝜑 → -∞ ∈ ℝ* )
7 nnuz ℕ = ( ℤ ‘ 1 )
8 1zzd ( 𝜑 → 1 ∈ ℤ )
9 4 2 fmptd ( 𝜑𝐺 : ℕ ⟶ ℝ )
10 9 ffvelrnda ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐺𝑘 ) ∈ ℝ )
11 7 8 10 serfre ( 𝜑 → seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
12 1 feq1i ( 𝑇 : ℕ ⟶ ℝ ↔ seq 1 ( + , 𝐺 ) : ℕ ⟶ ℝ )
13 11 12 sylibr ( 𝜑𝑇 : ℕ ⟶ ℝ )
14 1nn 1 ∈ ℕ
15 ffvelrn ( ( 𝑇 : ℕ ⟶ ℝ ∧ 1 ∈ ℕ ) → ( 𝑇 ‘ 1 ) ∈ ℝ )
16 13 14 15 sylancl ( 𝜑 → ( 𝑇 ‘ 1 ) ∈ ℝ )
17 16 rexrd ( 𝜑 → ( 𝑇 ‘ 1 ) ∈ ℝ* )
18 13 frnd ( 𝜑 → ran 𝑇 ⊆ ℝ )
19 ressxr ℝ ⊆ ℝ*
20 18 19 sstrdi ( 𝜑 → ran 𝑇 ⊆ ℝ* )
21 supxrcl ( ran 𝑇 ⊆ ℝ* → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
22 20 21 syl ( 𝜑 → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* )
23 16 mnfltd ( 𝜑 → -∞ < ( 𝑇 ‘ 1 ) )
24 13 ffnd ( 𝜑𝑇 Fn ℕ )
25 fnfvelrn ( ( 𝑇 Fn ℕ ∧ 1 ∈ ℕ ) → ( 𝑇 ‘ 1 ) ∈ ran 𝑇 )
26 24 14 25 sylancl ( 𝜑 → ( 𝑇 ‘ 1 ) ∈ ran 𝑇 )
27 supxrub ( ( ran 𝑇 ⊆ ℝ* ∧ ( 𝑇 ‘ 1 ) ∈ ran 𝑇 ) → ( 𝑇 ‘ 1 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
28 20 26 27 syl2anc ( 𝜑 → ( 𝑇 ‘ 1 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
29 6 17 22 23 28 xrltletrd ( 𝜑 → -∞ < sup ( ran 𝑇 , ℝ* , < ) )
30 xrrebnd ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* → ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( ran 𝑇 , ℝ* , < ) ∧ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) ) )
31 22 30 syl ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ↔ ( -∞ < sup ( ran 𝑇 , ℝ* , < ) ∧ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) ) )
32 29 31 mpbirand ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ↔ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) )
33 nfcv 𝑚 𝐴
34 nfcsb1v 𝑛 𝑚 / 𝑛 𝐴
35 csbeq1a ( 𝑛 = 𝑚𝐴 = 𝑚 / 𝑛 𝐴 )
36 33 34 35 cbviun 𝑛 ∈ ℕ 𝐴 = 𝑚 ∈ ℕ 𝑚 / 𝑛 𝐴
37 36 fveq2i ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) = ( vol* ‘ 𝑚 ∈ ℕ 𝑚 / 𝑛 𝐴 )
38 nfcv 𝑚 ( vol* ‘ 𝐴 )
39 nfcv 𝑛 vol*
40 39 34 nffv 𝑛 ( vol* ‘ 𝑚 / 𝑛 𝐴 )
41 35 fveq2d ( 𝑛 = 𝑚 → ( vol* ‘ 𝐴 ) = ( vol* ‘ 𝑚 / 𝑛 𝐴 ) )
42 38 40 41 cbvmpt ( 𝑛 ∈ ℕ ↦ ( vol* ‘ 𝐴 ) ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ 𝑚 / 𝑛 𝐴 ) )
43 2 42 eqtri 𝐺 = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ 𝑚 / 𝑛 𝐴 ) )
44 3 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
45 nfv 𝑚 𝐴 ⊆ ℝ
46 nfcv 𝑛
47 34 46 nfss 𝑛 𝑚 / 𝑛 𝐴 ⊆ ℝ
48 35 sseq1d ( 𝑛 = 𝑚 → ( 𝐴 ⊆ ℝ ↔ 𝑚 / 𝑛 𝐴 ⊆ ℝ ) )
49 45 47 48 cbvralw ( ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀ 𝑚 ∈ ℕ 𝑚 / 𝑛 𝐴 ⊆ ℝ )
50 44 49 sylib ( 𝜑 → ∀ 𝑚 ∈ ℕ 𝑚 / 𝑛 𝐴 ⊆ ℝ )
51 50 ad2antrr ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑚 ∈ ℕ 𝑚 / 𝑛 𝐴 ⊆ ℝ )
52 51 r19.21bi ( ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → 𝑚 / 𝑛 𝐴 ⊆ ℝ )
53 4 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) ∈ ℝ )
54 38 nfel1 𝑚 ( vol* ‘ 𝐴 ) ∈ ℝ
55 40 nfel1 𝑛 ( vol* ‘ 𝑚 / 𝑛 𝐴 ) ∈ ℝ
56 41 eleq1d ( 𝑛 = 𝑚 → ( ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ( vol* ‘ 𝑚 / 𝑛 𝐴 ) ∈ ℝ ) )
57 54 55 56 cbvralw ( ∀ 𝑛 ∈ ℕ ( vol* ‘ 𝐴 ) ∈ ℝ ↔ ∀ 𝑚 ∈ ℕ ( vol* ‘ 𝑚 / 𝑛 𝐴 ) ∈ ℝ )
58 53 57 sylib ( 𝜑 → ∀ 𝑚 ∈ ℕ ( vol* ‘ 𝑚 / 𝑛 𝐴 ) ∈ ℝ )
59 58 ad2antrr ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑚 ∈ ℕ ( vol* ‘ 𝑚 / 𝑛 𝐴 ) ∈ ℝ )
60 59 r19.21bi ( ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ 𝑚 / 𝑛 𝐴 ) ∈ ℝ )
61 simplr ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ )
62 simpr ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
63 1 43 52 60 61 62 ovoliunlem3 ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( vol* ‘ 𝑚 ∈ ℕ 𝑚 / 𝑛 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝑥 ) )
64 37 63 eqbrtrid ( ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ+ ) → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝑥 ) )
65 64 ralrimiva ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) → ∀ 𝑥 ∈ ℝ+ ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝑥 ) )
66 iunss ( 𝑛 ∈ ℕ 𝐴 ⊆ ℝ ↔ ∀ 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
67 44 66 sylibr ( 𝜑 𝑛 ∈ ℕ 𝐴 ⊆ ℝ )
68 ovolcl ( 𝑛 ∈ ℕ 𝐴 ⊆ ℝ → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* )
69 67 68 syl ( 𝜑 → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* )
70 xralrple ( ( ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) → ( ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝑥 ) ) )
71 69 70 sylan ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) → ( ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ ( sup ( ran 𝑇 , ℝ* , < ) + 𝑥 ) ) )
72 65 71 mpbird ( ( 𝜑 ∧ sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ ) → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )
73 72 ex ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
74 32 73 sylbird ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) < +∞ → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
75 nltpnft ( sup ( ran 𝑇 , ℝ* , < ) ∈ ℝ* → ( sup ( ran 𝑇 , ℝ* , < ) = +∞ ↔ ¬ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) )
76 22 75 syl ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) = +∞ ↔ ¬ sup ( ran 𝑇 , ℝ* , < ) < +∞ ) )
77 pnfge ( ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ∈ ℝ* → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ +∞ )
78 69 77 syl ( 𝜑 → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ +∞ )
79 breq2 ( sup ( ran 𝑇 , ℝ* , < ) = +∞ → ( ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ↔ ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ +∞ ) )
80 78 79 syl5ibrcom ( 𝜑 → ( sup ( ran 𝑇 , ℝ* , < ) = +∞ → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
81 76 80 sylbird ( 𝜑 → ( ¬ sup ( ran 𝑇 , ℝ* , < ) < +∞ → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) ) )
82 74 81 pm2.61d ( 𝜑 → ( vol* ‘ 𝑛 ∈ ℕ 𝐴 ) ≤ sup ( ran 𝑇 , ℝ* , < ) )