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 𝑇 , ℝ* , < ) )