voliun

Description: The Lebesgue measure function is countably additive. (Contributed by Mario Carneiro, 18-Mar-2014) (Proof shortened by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	voliun.1	$⊢ S = seq 1 (+ G)$
	voliun.2	$⊢ G = (n \in ℕ ⟼ vol (A))$
Assertion	voliun	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = sup (ran S ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		voliun.1	$⊢ S = seq 1 (+ G)$
2		voliun.2	$⊢ G = (n \in ℕ ⟼ vol (A))$
3		simpl	$⊢ (A \in dom vol \land vol (A) \in ℝ) \to A \in dom vol$
4	3	ralimi	$⊢ \forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \to \forall n \in ℕ A \in dom vol$
5	4	adantr	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to \forall n \in ℕ A \in dom vol$
6		eqid	$⊢ (n \in ℕ ⟼ A) = (n \in ℕ ⟼ A)$
7	6	fmpt	$⊢ \forall n \in ℕ A \in dom vol \leftrightarrow (n \in ℕ ⟼ A) : ℕ ⟶ dom vol$
8	5 7	sylib	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to (n \in ℕ ⟼ A) : ℕ ⟶ dom vol$
9	6	fvmpt2	$⊢ (n \in ℕ \land A \in dom vol) \to (n \in ℕ ⟼ A) (n) = A$
10	9	adantrr	$⊢ (n \in ℕ \land (A \in dom vol \land vol (A) \in ℝ)) \to (n \in ℕ ⟼ A) (n) = A$
11	10	ralimiaa	$⊢ \forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \to \forall n \in ℕ (n \in ℕ ⟼ A) (n) = A$
12		disjeq2	$⊢ \forall n \in ℕ (n \in ℕ ⟼ A) (n) = A \to (\underset{n \in ℕ}{Disj} (n \in ℕ ⟼ A) (n) \leftrightarrow \underset{n \in ℕ}{Disj} A)$
13	11 12	syl	$⊢ \forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \to (\underset{n \in ℕ}{Disj} (n \in ℕ ⟼ A) (n) \leftrightarrow \underset{n \in ℕ}{Disj} A)$
14	13	biimpar	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to \underset{n \in ℕ}{Disj} (n \in ℕ ⟼ A) (n)$
15		nfcv	$⊢ \underline{Ⅎ} i (n \in ℕ ⟼ A) (n)$
16		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ A) (i)$
17		fveq2	$⊢ n = i \to (n \in ℕ ⟼ A) (n) = (n \in ℕ ⟼ A) (i)$
18	15 16 17	cbvdisj	$⊢ \underset{n \in ℕ}{Disj} (n \in ℕ ⟼ A) (n) \leftrightarrow \underset{i \in ℕ}{Disj} (n \in ℕ ⟼ A) (i)$
19	14 18	sylib	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to \underset{i \in ℕ}{Disj} (n \in ℕ ⟼ A) (i)$
20		eqid	$⊢ (m \in ℕ ⟼ {vol}^{} (x \cap (n \in ℕ ⟼ A) (m))) = (m \in ℕ ⟼ {vol}^{} (x \cap (n \in ℕ ⟼ A) (m)))$
21		eqid	$⊢ seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n)))) = seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))))$
22		nfcv	$⊢ \underline{Ⅎ} m vol ((n \in ℕ ⟼ A) (n))$
23		nfcv	$⊢ \underline{Ⅎ} n vol$
24		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in ℕ ⟼ A) (m)$
25	23 24	nffv	$⊢ \underline{Ⅎ} n vol ((n \in ℕ ⟼ A) (m))$
26		2fveq3	$⊢ n = m \to vol ((n \in ℕ ⟼ A) (n)) = vol ((n \in ℕ ⟼ A) (m))$
27	22 25 26	cbvmpt	$⊢ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))) = (m \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (m)))$
28	9	fveq2d	$⊢ (n \in ℕ \land A \in dom vol) \to vol ((n \in ℕ ⟼ A) (n)) = vol (A)$
29	28	eleq1d	$⊢ (n \in ℕ \land A \in dom vol) \to (vol ((n \in ℕ ⟼ A) (n)) \in ℝ \leftrightarrow vol (A) \in ℝ)$
30	29	biimprd	$⊢ (n \in ℕ \land A \in dom vol) \to (vol (A) \in ℝ \to vol ((n \in ℕ ⟼ A) (n)) \in ℝ)$
31	30	impr	$⊢ (n \in ℕ \land (A \in dom vol \land vol (A) \in ℝ)) \to vol ((n \in ℕ ⟼ A) (n)) \in ℝ$
32	31	ralimiaa	$⊢ \forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \to \forall n \in ℕ vol ((n \in ℕ ⟼ A) (n)) \in ℝ$
33	32	adantr	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to \forall n \in ℕ vol ((n \in ℕ ⟼ A) (n)) \in ℝ$
34		nfv	$⊢ Ⅎ i vol ((n \in ℕ ⟼ A) (n)) \in ℝ$
35	23 16	nffv	$⊢ \underline{Ⅎ} n vol ((n \in ℕ ⟼ A) (i))$
36	35	nfel1	$⊢ Ⅎ n vol ((n \in ℕ ⟼ A) (i)) \in ℝ$
37		2fveq3	$⊢ n = i \to vol ((n \in ℕ ⟼ A) (n)) = vol ((n \in ℕ ⟼ A) (i))$
38	37	eleq1d	$⊢ n = i \to (vol ((n \in ℕ ⟼ A) (n)) \in ℝ \leftrightarrow vol ((n \in ℕ ⟼ A) (i)) \in ℝ)$
39	34 36 38	cbvralw	$⊢ \forall n \in ℕ vol ((n \in ℕ ⟼ A) (n)) \in ℝ \leftrightarrow \forall i \in ℕ vol ((n \in ℕ ⟼ A) (i)) \in ℝ$
40	33 39	sylib	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to \forall i \in ℕ vol ((n \in ℕ ⟼ A) (i)) \in ℝ$
41	8 19 20 21 27 40	voliunlem3	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to vol (⋃ ran (n \in ℕ ⟼ A)) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n)))) ℝ^{*} <)$
42		dfiun2g	$⊢ \forall n \in ℕ A \in dom vol \to ⋃_{n \in ℕ} A = ⋃ \{x \| \exists n \in ℕ x = A\}$
43	5 42	syl	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to ⋃_{n \in ℕ} A = ⋃ \{x \| \exists n \in ℕ x = A\}$
44	6	rnmpt	$⊢ ran (n \in ℕ ⟼ A) = \{x \| \exists n \in ℕ x = A\}$
45	44	unieqi	$⊢ ⋃ ran (n \in ℕ ⟼ A) = ⋃ \{x \| \exists n \in ℕ x = A\}$
46	43 45	eqtr4di	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to ⋃_{n \in ℕ} A = ⋃ ran (n \in ℕ ⟼ A)$
47	46	fveq2d	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = vol (⋃ ran (n \in ℕ ⟼ A))$
48		eqid	$⊢ ℕ = ℕ$
49	28	adantrr	$⊢ (n \in ℕ \land (A \in dom vol \land vol (A) \in ℝ)) \to vol ((n \in ℕ ⟼ A) (n)) = vol (A)$
50	49	ralimiaa	$⊢ \forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \to \forall n \in ℕ vol ((n \in ℕ ⟼ A) (n)) = vol (A)$
51	50	adantr	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to \forall n \in ℕ vol ((n \in ℕ ⟼ A) (n)) = vol (A)$
52		mpteq12	$⊢ (ℕ = ℕ \land \forall n \in ℕ vol ((n \in ℕ ⟼ A) (n)) = vol (A)) \to (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))) = (n \in ℕ ⟼ vol (A))$
53	48 51 52	sylancr	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))) = (n \in ℕ ⟼ vol (A))$
54	2 53	eqtr4id	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to G = (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n)))$
55	54	seqeq3d	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))))$
56	1 55	eqtrid	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to S = seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))))$
57	56	rneqd	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to ran S = ran seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n))))$
58	57	supeq1d	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to sup (ran S ℝ^{} <) = sup (ran seq 1 (+ (n \in ℕ ⟼ vol ((n \in ℕ ⟼ A) (n)))) ℝ^{} <)$
59	41 47 58	3eqtr4d	$⊢ (\forall n \in ℕ (A \in dom vol \land vol (A) \in ℝ) \land \underset{n \in ℕ}{Disj} A) \to vol (⋃_{n \in ℕ} A) = sup (ran S ℝ^{*} <)$

Metamath Proof Explorer

Theorem voliun

Proof