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	bilanri	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to \forall n \in ℕ \neg vol (E (n)) = +∞$
47	40	adantr	$⊢ ((φ \land n \in ℕ) \land \neg vol (E (n)) = +∞) \to vol (E (n)) \in [0, +∞]$
48	21	necon3bi	$⊢ \neg vol (E (n)) = +∞ \to vol (E (n)) \neq +∞$
49	48	adantl	$⊢ ((φ \land n \in ℕ) \land \neg vol (E (n)) = +∞) \to vol (E (n)) \neq +∞$
50		ge0xrre	$⊢ (vol (E (n)) \in [0, +∞] \land vol (E (n)) \neq +∞) \to vol (E (n)) \in ℝ$
51	47 49 50	syl2anc	$⊢ ((φ \land n \in ℕ) \land \neg vol (E (n)) = +∞) \to vol (E (n)) \in ℝ$
52	51	ex	$⊢ (φ \land n \in ℕ) \to (\neg vol (E (n)) = +∞ \to vol (E (n)) \in ℝ)$
53		renepnf	$⊢ vol (E (n)) \in ℝ \to vol (E (n)) \neq +∞$
54	53	neneqd	$⊢ vol (E (n)) \in ℝ \to \neg vol (E (n)) = +∞$
55	54	a1i	$⊢ (φ \land n \in ℕ) \to (vol (E (n)) \in ℝ \to \neg vol (E (n)) = +∞)$
56	52 55	impbid	$⊢ (φ \land n \in ℕ) \to (\neg vol (E (n)) = +∞ \leftrightarrow vol (E (n)) \in ℝ)$
57	56	ralbidva	$⊢ φ \to (\forall n \in ℕ \neg vol (E (n)) = +∞ \leftrightarrow \forall n \in ℕ vol (E (n)) \in ℝ)$
58	57	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 ℝ)$
59	46 58	mpbid	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to \forall n \in ℕ vol (E (n)) \in ℝ$
60		nfra1	$⊢ Ⅎ n \forall n \in ℕ vol (E (n)) \in ℝ$
61	5 60	nfan	$⊢ Ⅎ n (φ \land \forall n \in ℕ vol (E (n)) \in ℝ)$
62	13	adantlr	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to E (n) \in dom vol$
63		rspa	$⊢ (\forall n \in ℕ vol (E (n)) \in ℝ \land n \in ℕ) \to vol (E (n)) \in ℝ$
64	63	adantll	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in ℝ$
65	62 64	jca	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to (E (n) \in dom vol \land vol (E (n)) \in ℝ)$
66	65	ex	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to (n \in ℕ \to (E (n) \in dom vol \land vol (E (n)) \in ℝ))$
67	61 66	ralrimi	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to \forall n \in ℕ (E (n) \in dom vol \land vol (E (n)) \in ℝ)$
68	4	adantr	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to \underset{n \in ℕ}{Disj} E (n)$
69	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 ℝ^{*} <)$
70	67 68 69	syl2anc	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to vol (⋃_{n \in ℕ} E (n)) = sup (ran S ℝ^{*} <)$
71		1zzd	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to 1 \in ℤ$
72		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
73		nfv	$⊢ Ⅎ n m \in ℕ$
74	61 73	nfan	$⊢ Ⅎ n ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ)$
75		nfv	$⊢ Ⅎ n vol (E (m)) \in [0, +∞)$
76	74 75	nfim	$⊢ Ⅎ n (((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ) \to vol (E (m)) \in [0, +∞))$
77		eleq1w	$⊢ n = m \to (n \in ℕ \leftrightarrow m \in ℕ)$
78	77	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 ℕ))$
79		2fveq3	$⊢ n = m \to vol (E (n)) = vol (E (m))$
80	79	eleq1d	$⊢ n = m \to (vol (E (n)) \in [0, +∞) \leftrightarrow vol (E (m)) \in [0, +∞))$
81	78 80	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, +∞)))$
82		0xr	$⊢ 0 \in ℝ^{*}$
83	82	a1i	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to 0 \in ℝ^{*}$
84		pnfxr	$⊢ +∞ \in ℝ^{*}$
85	84	a1i	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to +∞ \in ℝ^{*}$
86	64	rexrd	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in ℝ^{*}$
87		volge0	$⊢ E (n) \in dom vol \to 0 \leq vol (E (n))$
88	13 87	syl	$⊢ (φ \land n \in ℕ) \to 0 \leq vol (E (n))$
89	88	adantlr	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to 0 \leq vol (E (n))$
90	64	ltpnfd	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) < +∞$
91	83 85 86 89 90	elicod	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land n \in ℕ) \to vol (E (n)) \in [0, +∞)$
92	76 81 91	chvarfv	$⊢ ((φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \land m \in ℕ) \to vol (E (m)) \in [0, +∞)$
93	79	cbvmptv	$⊢ (n \in ℕ ⟼ vol (E (n))) = (m \in ℕ ⟼ vol (E (m)))$
94	92 93	fmptd	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to (n \in ℕ ⟼ vol (E (n))) : ℕ ⟶ [0, +∞)$
95		seqeq3	$⊢ G = (n \in ℕ ⟼ vol (E (n))) \to seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol (E (n))))$
96	2 95	ax-mp	$⊢ seq 1 (+ G) = seq 1 (+ (n \in ℕ ⟼ vol (E (n))))$
97	1 96	eqtri	$⊢ S = seq 1 (+ (n \in ℕ ⟼ vol (E (n))))$
98	71 72 94 97	sge0seq	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to sum^((n \in ℕ ⟼ vol (E (n)))) = sup (ran S ℝ^{*} <)$
99	70 98	eqtr4d	$⊢ (φ \land \forall n \in ℕ vol (E (n)) \in ℝ) \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$
100	59 99	syldan	$⊢ (φ \land \neg \exists n \in ℕ vol (E (n)) = +∞) \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$
101	44 100	pm2.61dan	$⊢ φ \to vol (⋃_{n \in ℕ} E (n)) = sum^((n \in ℕ ⟼ vol (E (n))))$

Metamath Proof Explorer

Theorem voliunsge0lem

Proof