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 \in ℕ ⟼ {vol}^{*} (A))$
	ovoliun.a	$⊢ (φ \land n \in ℕ) \to A \subseteq ℝ$
	ovoliun.v	$⊢ (φ \land n \in ℕ) \to {vol}^{*} (A) \in ℝ$
Assertion	ovoliun	$⊢ φ \to {vol}^{} (⋃_{n \in ℕ} A) \leq sup (ran T ℝ^{} <)$

Proof

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

Metamath Proof Explorer

Theorem ovoliun

Proof