voliunsge0lem

Description: The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	voliunsge0lem.s	$⊢ S = seq 1 (+ G)$
	voliunsge0lem.g	$⊢ G = (n \in ℕ ⟼ vol (E (n)))$
	voliunsge0lem.e	$⊢ φ \to E : ℕ ⟶ dom vol$
	voliunsge0lem.d	$⊢ φ \to \underset{n \in ℕ}{Disj} E (n)$
Assertion	voliunsge0lem	$⊢ φ \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$

Proof

Step	Hyp	Ref	Expression
1		voliunsge0lem.s	$⊢ S = seq 1 (+ G)$
2		voliunsge0lem.g	$⊢ G = (n \in ℕ ⟼ vol (E (n)))$
3		voliunsge0lem.e	$⊢ φ \to E : ℕ ⟶ dom vol$
4		voliunsge0lem.d	$⊢ φ \to \underset{n \in ℕ}{Disj} E (n)$
5		nfv	$⊢ Ⅎ n φ$
6		nfcv	$⊢ \underline{Ⅎ} n vol$
7		nfiu1	$⊢ \underline{Ⅎ} n ⋃_{n \in ℕ} E (n)$
8	6 7	nffv	$⊢ \underline{Ⅎ} n vol (⋃_{n \in ℕ} E (n))$
9	8	nfeq1	$⊢ Ⅎ n vol (⋃_{n \in ℕ} E (n)) = +∞$
10		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
11		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
12	11	a1i	$⊢ φ \to vol : dom vol ⟶ [0, +∞]$
13	3	ffvelcdmda	$⊢ (φ \land n \in ℕ) \to E (n) \in dom vol$
14	13	ralrimiva	$⊢ φ \to \forall n \in ℕ E (n) \in dom vol$
15		iunmbl	$⊢ \forall n \in ℕ E (n) \in dom vol \to ⋃_{n \in ℕ} E (n) \in dom vol$
16	14 15	syl	$⊢ φ \to ⋃_{n \in ℕ} E (n) \in dom vol$
17	12 16	ffvelcdmd	$⊢ φ \to vol (⋃_{n \in ℕ} E (n)) \in [0, +∞]$
18	10 17	sselid	$⊢ φ \to vol (⋃_{n \in ℕ} E (n)) \in ℝ^{*}$
19	18	adantr	$⊢ (φ \land n \in ℕ) \to vol (⋃_{n \in ℕ} E (n)) \in ℝ^{*}$
20	19	3adant3	$⊢ (φ \land n \in ℕ \land vol (E (n)) = +∞) \to vol (⋃_{n \in ℕ} E (n)) \in ℝ^{*}$
21		id	$⊢ vol (E (n)) = +∞ \to vol (E (n)) = +∞$
22	21	eqcomd	$⊢ vol (E (n)) = +∞ \to +∞ = vol (E (n))$
23	22	3ad2ant3	$⊢ (φ \land n \in ℕ \land vol (E (n)) = +∞) \to +∞ = vol (E (n))$
24	16	adantr	$⊢ (φ \land n \in ℕ) \to ⋃_{n \in ℕ} E (n) \in dom vol$
25		ssiun2	$⊢ n \in ℕ \to E (n) \subseteq ⋃_{n \in ℕ} E (n)$
26	25	adantl	$⊢ (φ \land n \in ℕ) \to E (n) \subseteq ⋃_{n \in ℕ} E (n)$
27		volss	$⊢ (E (n) \in dom vol \land ⋃_{n \in ℕ} E (n) \in dom vol \land E (n) \subseteq ⋃_{n \in ℕ} E (n)) \to vol (E (n)) \leq vol (⋃_{n \in ℕ} E (n))$
28	13 24 26 27	syl3anc	$⊢ (φ \land n \in ℕ) \to vol (E (n)) \leq vol (⋃_{n \in ℕ} E (n))$
29	28	3adant3	$⊢ (φ \land n \in ℕ \land vol (E (n)) = +∞) \to vol (E (n)) \leq vol (⋃_{n \in ℕ} E (n))$
30	23 29	eqbrtrd	$⊢ (φ \land n \in ℕ \land vol (E (n)) = +∞) \to +∞ \leq vol (⋃_{n \in ℕ} E (n))$
31	20 30	xrgepnfd	$⊢ (φ \land n \in ℕ \land vol (E (n)) = +∞) \to vol (⋃_{n \in ℕ} E (n)) = +∞$
32	31	3exp	$⊢ φ \to (n \in ℕ \to (vol (E (n)) = +∞ \to vol (⋃_{n \in ℕ} E (n)) = +∞))$
33	5 9 32	rexlimd	$⊢ φ \to (\exists n \in ℕ vol (E (n)) = +∞ \to vol (⋃_{n \in ℕ} E (n)) = +∞)$
34	33	imp	$⊢ (φ \land \exists n \in ℕ vol (E (n)) = +∞) \to vol (⋃_{n \in ℕ} E (n)) = +∞$
35		nfre1	$⊢ Ⅎ n \exists n \in ℕ vol (E (n)) = +∞$
36	5 35	nfan	$⊢ Ⅎ n (φ \land \exists n \in ℕ vol (E (n)) = +∞)$
37		nnex	$⊢ ℕ \in V$
38	37	a1i	$⊢ (φ \land \exists n \in ℕ vol (E (n)) = +∞) \to ℕ \in V$
39	11	a1i	$⊢ (φ \land n \in ℕ) \to vol : dom vol ⟶ [0, +∞]$
40	39 13	ffvelcdmd	$⊢ (φ \land n \in ℕ) \to vol (E (n)) \in [0, +∞]$
41	40	adantlr	$⊢ ((φ \land \exists n \in ℕ vol (E (n)) = +∞) \land n \in ℕ) \to vol (E (n)) \in [0, +∞]$
42		simpr	$⊢ (φ \land \exists n \in ℕ vol (E (n)) = +∞) \to \exists n \in ℕ vol (E (n)) = +∞$
43	36 38 41 42	sge0pnfmpt	$⊢ (φ \land \exists n \in ℕ vol (E (n)) = +∞) \to sum^((n \in ℕ ⟼ vol (E (n)))) = +∞$
44	34 43	eqtr4d	$⊢ (φ \land \exists n \in ℕ vol (E (n)) = +∞) \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$
45		ralnex	$⊢ \forall n \in ℕ \neg vol (E (n)) = +∞ \leftrightarrow \neg \exists n \in ℕ vol (E (n)) = +∞$
46	45	biimpri	$⊢ \neg \exists n \in ℕ vol (E (n)) = +∞ \to \forall n \in ℕ \neg vol (E (n)) = +∞$
47	46	adantl	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to \forall n \in ℕ \neg vol (E (n)) = +∞$
48	40	adantr	$⊢ ((φ \land n \in ℕ) \land \neg vol (E (n)) = +∞) \to vol (E (n)) \in [0, +∞]$
49	21	necon3bi	$⊢ \neg vol (E (n)) = +∞ \to vol (E (n)) \neq +∞$
50	49	adantl	$⊢ ((φ \land n \in ℕ) \land \neg vol (E (n)) = +∞) \to vol (E (n)) \neq +∞$
51		ge0xrre	$⊢ (vol (E (n)) \in [0, +∞] \land vol (E (n)) \neq +∞) \to vol (E (n)) \in ℝ$
52	48 50 51	syl2anc	$⊢ ((φ \land n \in ℕ) \land \neg vol (E (n)) = +∞) \to vol (E (n)) \in ℝ$
53	52	ex	$⊢ (φ \land n \in ℕ) \to (\neg vol (E (n)) = +∞ \to vol (E (n)) \in ℝ)$
54		renepnf	$⊢ vol (E (n)) \in ℝ \to vol (E (n)) \neq +∞$
55	54	neneqd	$⊢ vol (E (n)) \in ℝ \to \neg vol (E (n)) = +∞$
56	55	a1i	$⊢ (φ \land n \in ℕ) \to (vol (E (n)) \in ℝ \to \neg vol (E (n)) = +∞)$
57	53 56	impbid	$⊢ (φ \land n \in ℕ) \to (\neg vol (E (n)) = +∞ \leftrightarrow vol (E (n)) \in ℝ)$
58	57	ralbidva	$⊢ φ \to (\forall n \in ℕ \neg vol (E (n)) = +∞ \leftrightarrow \forall n \in ℕ vol (E (n)) \in ℝ)$
59	58	adantr	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to (\forall n \in ℕ \neg vol (E (n)) = +∞ \leftrightarrow \forall n \in ℕ vol (E (n)) \in ℝ)$
60	47 59	mpbid	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to \forall n \in ℕ vol (E (n)) \in ℝ$
61		nfra1	$⊢ Ⅎ n \forall n \in ℕ vol (E (n)) \in ℝ$
62	5 61	nfan	$⊢ Ⅎ n (φ \land \forall n \in ℕ vol (E (n)) \in ℝ)$
63	13	adantlr	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to E (n) \in dom vol$
64		rspa	$⊢ (\forall n \in ℕ vol (E (n)) \in ℝ \land n \in ℕ) \to vol (E (n)) \in ℝ$
65	64	adantll	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in ℝ$
66	63 65	jca	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to (E (n) \in dom vol \land vol (E (n)) \in ℝ)$
67	66	ex	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to (n \in ℕ \to (E (n) \in dom vol \land vol (E (n)) \in ℝ))$
68	62 67	ralrimi	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to \forall n \in ℕ (E (n) \in dom vol \land vol (E (n)) \in ℝ)$
69	4	adantr	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to \underset{n \in ℕ}{Disj} E (n)$
70	1 2	voliun	$⊢ (\forall n \in ℕ (E (n) \in dom vol \land vol (E (n)) \in ℝ) \land \underset{n \in ℕ}{Disj} E (n)) \to vol (⋃_{n \in ℕ} E (n)) = sup (ran S ℝ^{*} <)$
71	68 69 70	syl2anc	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to vol (⋃_{n \in ℕ} E (n)) = sup (ran S ℝ^{*} <)$
72		1zzd	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to 1 \in ℤ$
73		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
74		nfv	$⊢ Ⅎ n m \in ℕ$
75	62 74	nfan	$⊢ Ⅎ n ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ)$
76		nfv	$⊢ Ⅎ n vol (E (m)) \in [0, +∞)$
77	75 76	nfim	$⊢ Ⅎ n (((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ) \to vol (E (m)) \in [0, +∞))$
78		eleq1w	$⊢ n = m \to (n \in ℕ \leftrightarrow m \in ℕ)$
79	78	anbi2d	$⊢ n = m \to (((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \leftrightarrow ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ))$
80		2fveq3	$⊢ n = m \to vol (E (n)) = vol (E (m))$
81	80	eleq1d	$⊢ n = m \to (vol (E (n)) \in [0, +∞) \leftrightarrow vol (E (m)) \in [0, +∞))$
82	79 81	imbi12d	$⊢ n = m \to ((((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in [0, +∞)) \leftrightarrow (((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ) \to vol (E (m)) \in [0, +∞)))$
83		0xr	$⊢ 0 \in ℝ^{*}$
84	83	a1i	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to 0 \in ℝ^{*}$
85		pnfxr	$⊢ +∞ \in ℝ^{*}$
86	85	a1i	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to +∞ \in ℝ^{*}$
87	65	rexrd	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in ℝ^{*}$
88		volge0	$⊢ E (n) \in dom vol \to 0 \leq vol (E (n))$
89	13 88	syl	$⊢ (φ \land n \in ℕ) \to 0 \leq vol (E (n))$
90	89	adantlr	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to 0 \leq vol (E (n))$
91	65	ltpnfd	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) < +∞$
92	84 86 87 90 91	elicod	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in [0, +∞)$
93	77 82 92	chvarfv	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ) \to vol (E (m)) \in [0, +∞)$
94	80	cbvmptv	$⊢ (n \in ℕ ⟼ vol (E (n))) = (m \in ℕ ⟼ vol (E (m)))$
95	93 94	fmptd	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to (n \in ℕ ⟼ vol (E (n))) : ℕ ⟶ [0, +∞)$
96		seqeq3	$⊢ G = (n \in ℕ ⟼ vol (E (n))) \to seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol (E (n))))$
97	2 96	ax-mp	$⊢ seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol (E (n))))$
98	1 97	eqtri	$⊢ S = seq 1 (+ (n \in ℕ ⟼ vol (E (n))))$
99	72 73 95 98	sge0seq	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to sum^((n \in ℕ ⟼ vol (E (n)))) = sup (ran S ℝ^{*} <)$
100	71 99	eqtr4d	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$
101	60 100	syldan	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$
102	44 101	pm2.61dan	$⊢ φ \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$

Metamath Proof Explorer

Theorem voliunsge0lem

Proof