ovoliunnul

Description: A countable union of nullsets is null. (Contributed by Mario Carneiro, 8-Apr-2015)

		Ref	Expression
	Assertion	ovoliunnul	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to {vol}^{} (⋃_{n \in A} B) = 0$

Proof

Step	Hyp	Ref	Expression
1		iuneq1	$⊢ A = \emptyset \to ⋃_{n \in A} B = ⋃_{n \in \emptyset} B$
2		0iun	$⊢ ⋃_{n \in \emptyset} B = \emptyset$
3	1 2	eqtrdi	$⊢ A = \emptyset \to ⋃_{n \in A} B = \emptyset$
4	3	fveq2d	$⊢ A = \emptyset \to {vol}^{} (⋃_{n \in A} B) = {vol}^{} (\emptyset)$
5		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
6	4 5	eqtrdi	$⊢ A = \emptyset \to {vol}^{*} (⋃_{n \in A} B) = 0$
7	6	a1i	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to (A = \emptyset \to {vol}^{} (⋃_{n \in A} B) = 0)$
8		reldom	$⊢ Rel ≼$
9	8	brrelex1i	$⊢ A ≼ ℕ \to A \in V$
10	9	adantr	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \to A \in V$
11		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
12	10 11	syl	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
13		fodomr	$⊢ (\emptyset ≺ A \land A ≼ ℕ) \to \exists f f : ℕ \underset{onto}{⟶} A$
14	13	expcom	$⊢ A ≼ ℕ \to (\emptyset ≺ A \to \exists f f : ℕ \underset{onto}{⟶} A)$
15	14	adantr	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \to (\emptyset ≺ A \to \exists f f : ℕ \underset{onto}{⟶} A)$
16		eliun	$⊢ x \in ⋃_{n \in A} B \leftrightarrow \exists n \in A x \in B$
17		nfv	$⊢ Ⅎ n f : ℕ \underset{onto}{⟶} A$
18		nfcv	$⊢ \underline{Ⅎ} n ℕ$
19		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ f (k) / n ⦌ B$
20	18 19	nfiun	$⊢ \underline{Ⅎ} n ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B$
21	20	nfcri	$⊢ Ⅎ n x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B$
22		foelrn	$⊢ (f : ℕ \underset{onto}{⟶} A \land n \in A) \to \exists k \in ℕ n = f (k)$
23	22	ex	$⊢ f : ℕ \underset{onto}{⟶} A \to (n \in A \to \exists k \in ℕ n = f (k))$
24		csbeq1a	$⊢ n = f (k) \to B = ⦋ f (k) / n ⦌ B$
25	24	adantl	$⊢ (f : ℕ \underset{onto}{⟶} A \land n = f (k)) \to B = ⦋ f (k) / n ⦌ B$
26	25	eleq2d	$⊢ (f : ℕ \underset{onto}{⟶} A \land n = f (k)) \to (x \in B \leftrightarrow x \in ⦋ f (k) / n ⦌ B)$
27	26	biimpd	$⊢ (f : ℕ \underset{onto}{⟶} A \land n = f (k)) \to (x \in B \to x \in ⦋ f (k) / n ⦌ B)$
28	27	impancom	$⊢ (f : ℕ \underset{onto}{⟶} A \land x \in B) \to (n = f (k) \to x \in ⦋ f (k) / n ⦌ B)$
29	28	reximdv	$⊢ (f : ℕ \underset{onto}{⟶} A \land x \in B) \to (\exists k \in ℕ n = f (k) \to \exists k \in ℕ x \in ⦋ f (k) / n ⦌ B)$
30		eliun	$⊢ x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \leftrightarrow \exists k \in ℕ x \in ⦋ f (k) / n ⦌ B$
31	29 30	imbitrrdi	$⊢ (f : ℕ \underset{onto}{⟶} A \land x \in B) \to (\exists k \in ℕ n = f (k) \to x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)$
32	31	ex	$⊢ f : ℕ \underset{onto}{⟶} A \to (x \in B \to (\exists k \in ℕ n = f (k) \to x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B))$
33	32	com23	$⊢ f : ℕ \underset{onto}{⟶} A \to (\exists k \in ℕ n = f (k) \to (x \in B \to x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B))$
34	23 33	syld	$⊢ f : ℕ \underset{onto}{⟶} A \to (n \in A \to (x \in B \to x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B))$
35	17 21 34	rexlimd	$⊢ f : ℕ \underset{onto}{⟶} A \to (\exists n \in A x \in B \to x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)$
36	16 35	biimtrid	$⊢ f : ℕ \underset{onto}{⟶} A \to (x \in ⋃_{n \in A} B \to x \in ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)$
37	36	ssrdv	$⊢ f : ℕ \underset{onto}{⟶} A \to ⋃_{n \in A} B \subseteq ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B$
38	37	adantl	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to ⋃_{n \in A} B \subseteq ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B$
39		fof	$⊢ f : ℕ \underset{onto}{⟶} A \to f : ℕ ⟶ A$
40	39	adantl	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to f : ℕ ⟶ A$
41	40	ffvelcdmda	$⊢ (((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \land k \in ℕ) \to f (k) \in A$
42		simpllr	$⊢ (((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \land k \in ℕ) \to \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)$
43		nfcv	$⊢ \underline{Ⅎ} n ℝ$
44	19 43	nfss	$⊢ Ⅎ n ⦋ f (k) / n ⦌ B \subseteq ℝ$
45		nfcv	$⊢ \underline{Ⅎ} n {vol}^{*}$
46	45 19	nffv	$⊢ \underline{Ⅎ} n {vol}^{*} (⦋ f (k) / n ⦌ B)$
47	46	nfeq1	$⊢ Ⅎ n {vol}^{*} (⦋ f (k) / n ⦌ B) = 0$
48	44 47	nfan	$⊢ Ⅎ n (⦋ f (k) / n ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ f (k) / n ⦌ B) = 0)$
49	24	sseq1d	$⊢ n = f (k) \to (B \subseteq ℝ \leftrightarrow ⦋ f (k) / n ⦌ B \subseteq ℝ)$
50	24	fveqeq2d	$⊢ n = f (k) \to ({vol}^{} (B) = 0 \leftrightarrow {vol}^{} (⦋ f (k) / n ⦌ B) = 0)$
51	49 50	anbi12d	$⊢ n = f (k) \to ((B \subseteq ℝ \land {vol}^{} (B) = 0) \leftrightarrow (⦋ f (k) / n ⦌ B \subseteq ℝ \land {vol}^{} (⦋ f (k) / n ⦌ B) = 0))$
52	48 51	rspc	$⊢ f (k) \in A \to (\forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0) \to (⦋ f (k) / n ⦌ B \subseteq ℝ \land {vol}^{} (⦋ f (k) / n ⦌ B) = 0))$
53	41 42 52	sylc	$⊢ (((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \land k \in ℕ) \to (⦋ f (k) / n ⦌ B \subseteq ℝ \land {vol}^{} (⦋ f (k) / n ⦌ B) = 0)$
54	53	simpld	$⊢ (((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \land k \in ℕ) \to ⦋ f (k) / n ⦌ B \subseteq ℝ$
55	54	ralrimiva	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to \forall k \in ℕ ⦋ f (k) / n ⦌ B \subseteq ℝ$
56		iunss	$⊢ ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \subseteq ℝ \leftrightarrow \forall k \in ℕ ⦋ f (k) / n ⦌ B \subseteq ℝ$
57	55 56	sylibr	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{*} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \subseteq ℝ$
58		eqid	$⊢ seq 1 (+ (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B))) = seq 1 (+ (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B)))$
59		eqid	$⊢ (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B)) = (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B))$
60	53	simprd	$⊢ (((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \land k \in ℕ) \to {vol}^{} (⦋ f (k) / n ⦌ B) = 0$
61		0re	$⊢ 0 \in ℝ$
62	60 61	eqeltrdi	$⊢ (((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \land k \in ℕ) \to {vol}^{} (⦋ f (k) / n ⦌ B) \in ℝ$
63	60	mpteq2dva	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B)) = (k \in ℕ ⟼ 0)$
64		fconstmpt	$⊢ ℕ \times \{0\} = (k \in ℕ ⟼ 0)$
65		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
66	65	xpeq1i	$⊢ ℕ \times \{0\} = ℤ_{\geq 1} \times \{0\}$
67	64 66	eqtr3i	$⊢ (k \in ℕ ⟼ 0) = ℤ_{\geq 1} \times \{0\}$
68	63 67	eqtrdi	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B)) = ℤ_{\geq 1} \times \{0\}$
69	68	seqeq3d	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to seq 1 (+ (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B))) = seq 1 (+ (ℤ_{\geq 1} \times \{0\}))$
70		1z	$⊢ 1 \in ℤ$
71		serclim0	$⊢ 1 \in ℤ \to seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0$
72		seqex	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) \in V$
73		c0ex	$⊢ 0 \in V$
74	72 73	breldm	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) ⇝ 0 \to seq 1 (+ (ℤ_{\geq 1} \times \{0\})) \in dom ⇝$
75	70 71 74	mp2b	$⊢ seq 1 (+ (ℤ_{\geq 1} \times \{0\})) \in dom ⇝$
76	69 75	eqeltrdi	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to seq 1 (+ (k \in ℕ ⟼ {vol}^{} (⦋ f (k) / n ⦌ B))) \in dom ⇝$
77	58 59 54 62 76	ovoliun2	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \leq \sum_{k \in ℕ} {vol}^{*} (⦋ f (k) / n ⦌ B)$
78	60	sumeq2dv	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to \sum_{k \in ℕ} {vol}^{} (⦋ f (k) / n ⦌ B) = \sum_{k \in ℕ} 0$
79	65	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
80	79	orci	$⊢ (ℕ \subseteq ℤ_{\geq 1} \lor ℕ \in Fin)$
81		sumz	$⊢ (ℕ \subseteq ℤ_{\geq 1} \lor ℕ \in Fin) \to \sum_{k \in ℕ} 0 = 0$
82	80 81	ax-mp	$⊢ \sum_{k \in ℕ} 0 = 0$
83	78 82	eqtrdi	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to \sum_{k \in ℕ} {vol}^{} (⦋ f (k) / n ⦌ B) = 0$
84	77 83	breqtrd	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \leq 0$
85		ovolge0	$⊢ ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \subseteq ℝ \to 0 \leq {vol}^{*} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)$
86	57 85	syl	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to 0 \leq {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)$
87		ovolcl	$⊢ ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \subseteq ℝ \to {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \in ℝ^{}$
88	57 87	syl	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \in ℝ^{*}$
89		0xr	$⊢ 0 \in ℝ^{*}$
90		xrletri3	$⊢ ({vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \in ℝ^{} \land 0 \in ℝ^{}) \to ({vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) = 0 \leftrightarrow ({vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \leq 0 \land 0 \leq {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)))$
91	88 89 90	sylancl	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to ({vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) = 0 \leftrightarrow ({vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) \leq 0 \land 0 \leq {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B)))$
92	84 86 91	mpbir2and	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) = 0$
93		ovolssnul	$⊢ (⋃_{n \in A} B \subseteq ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \land ⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B \subseteq ℝ \land {vol}^{} (⋃_{k \in ℕ} ⦋ f (k) / n ⦌ B) = 0) \to {vol}^{} (⋃_{n \in A} B) = 0$
94	38 57 92 93	syl3anc	$⊢ ((A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \land f : ℕ \underset{onto}{⟶} A) \to {vol}^{} (⋃_{n \in A} B) = 0$
95	94	ex	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to (f : ℕ \underset{onto}{⟶} A \to {vol}^{} (⋃_{n \in A} B) = 0)$
96	95	exlimdv	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to (\exists f f : ℕ \underset{onto}{⟶} A \to {vol}^{} (⋃_{n \in A} B) = 0)$
97	15 96	syld	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to (\emptyset ≺ A \to {vol}^{} (⋃_{n \in A} B) = 0)$
98	12 97	sylbird	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to (A \neq \emptyset \to {vol}^{} (⋃_{n \in A} B) = 0)$
99	7 98	pm2.61dne	$⊢ (A ≼ ℕ \land \forall n \in A (B \subseteq ℝ \land {vol}^{} (B) = 0)) \to {vol}^{} (⋃_{n \in A} B) = 0$

Metamath Proof Explorer

Theorem ovoliunnul

Proof