ovolfiniun

Description: The Lebesgue outer measure function is finitely sub-additive. Finite sum version. (Contributed by Mario Carneiro, 19-Jun-2014)

		Ref	Expression
	Assertion	ovolfiniun	$⊢ (A \in Fin \land \forall k \in A (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (⋃_{k \in A} B) \leq \sum_{k \in A} {vol}^{*} (B)$

Proof

Step	Hyp	Ref	Expression
1		raleq	$⊢ x = \emptyset \to (\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \leftrightarrow \forall k \in \emptyset (B \subseteq ℝ \land {vol}^{} (B) \in ℝ))$
2		iuneq1	$⊢ x = \emptyset \to ⋃_{k \in x} B = ⋃_{k \in \emptyset} B$
3	2	fveq2d	$⊢ x = \emptyset \to {vol}^{} (⋃_{k \in x} B) = {vol}^{} (⋃_{k \in \emptyset} B)$
4		sumeq1	$⊢ x = \emptyset \to \sum_{k \in x} {vol}^{} (B) = \sum_{k \in \emptyset} {vol}^{} (B)$
5	3 4	breq12d	$⊢ x = \emptyset \to ({vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B) \leftrightarrow {vol}^{} (⋃_{k \in \emptyset} B) \leq \sum_{k \in \emptyset} {vol}^{} (B))$
6	1 5	imbi12d	$⊢ x = \emptyset \to ((\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B)) \leftrightarrow (\forall k \in \emptyset (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in \emptyset} B) \leq \sum_{k \in \emptyset} {vol}^{} (B)))$
7		raleq	$⊢ x = y \to (\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \leftrightarrow \forall k \in y (B \subseteq ℝ \land {vol}^{} (B) \in ℝ))$
8		iuneq1	$⊢ x = y \to ⋃_{k \in x} B = ⋃_{k \in y} B$
9	8	fveq2d	$⊢ x = y \to {vol}^{} (⋃_{k \in x} B) = {vol}^{} (⋃_{k \in y} B)$
10		sumeq1	$⊢ x = y \to \sum_{k \in x} {vol}^{} (B) = \sum_{k \in y} {vol}^{} (B)$
11	9 10	breq12d	$⊢ x = y \to ({vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B) \leftrightarrow {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))$
12	7 11	imbi12d	$⊢ x = y \to ((\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B)) \leftrightarrow (\forall k \in y (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B)))$
13		raleq	$⊢ x = y \cup \{z\} \to (\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \leftrightarrow \forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ))$
14		iuneq1	$⊢ x = y \cup \{z\} \to ⋃_{k \in x} B = ⋃_{k \in y \cup \{z\}} B$
15	14	fveq2d	$⊢ x = y \cup \{z\} \to {vol}^{} (⋃_{k \in x} B) = {vol}^{} (⋃_{k \in y \cup \{z\}} B)$
16		sumeq1	$⊢ x = y \cup \{z\} \to \sum_{k \in x} {vol}^{} (B) = \sum_{k \in y \cup \{z\}} {vol}^{} (B)$
17	15 16	breq12d	$⊢ x = y \cup \{z\} \to ({vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B) \leftrightarrow {vol}^{} (⋃_{k \in y \cup \{z\}} B) \leq \sum_{k \in y \cup \{z\}} {vol}^{} (B))$
18	13 17	imbi12d	$⊢ x = y \cup \{z\} \to ((\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B)) \leftrightarrow (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y \cup \{z\}} B) \leq \sum_{k \in y \cup \{z\}} {vol}^{} (B)))$
19		raleq	$⊢ x = A \to (\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \leftrightarrow \forall k \in A (B \subseteq ℝ \land {vol}^{} (B) \in ℝ))$
20		iuneq1	$⊢ x = A \to ⋃_{k \in x} B = ⋃_{k \in A} B$
21	20	fveq2d	$⊢ x = A \to {vol}^{} (⋃_{k \in x} B) = {vol}^{} (⋃_{k \in A} B)$
22		sumeq1	$⊢ x = A \to \sum_{k \in x} {vol}^{} (B) = \sum_{k \in A} {vol}^{} (B)$
23	21 22	breq12d	$⊢ x = A \to ({vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B) \leftrightarrow {vol}^{} (⋃_{k \in A} B) \leq \sum_{k \in A} {vol}^{} (B))$
24	19 23	imbi12d	$⊢ x = A \to ((\forall k \in x (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in x} B) \leq \sum_{k \in x} {vol}^{} (B)) \leftrightarrow (\forall k \in A (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in A} B) \leq \sum_{k \in A} {vol}^{} (B)))$
25		0le0	$⊢ 0 \leq 0$
26		0iun	$⊢ ⋃_{k \in \emptyset} B = \emptyset$
27	26	fveq2i	$⊢ {vol}^{} (⋃_{k \in \emptyset} B) = {vol}^{} (\emptyset)$
28		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
29	27 28	eqtri	$⊢ {vol}^{*} (⋃_{k \in \emptyset} B) = 0$
30		sum0	$⊢ \sum_{k \in \emptyset} {vol}^{*} (B) = 0$
31	25 29 30	3brtr4i	$⊢ {vol}^{} (⋃_{k \in \emptyset} B) \leq \sum_{k \in \emptyset} {vol}^{} (B)$
32	31	a1i	$⊢ \forall k \in \emptyset (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in \emptyset} B) \leq \sum_{k \in \emptyset} {vol}^{*} (B)$
33		ssun1	$⊢ y \subseteq y \cup \{z\}$
34		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to \forall k \in y (B \subseteq ℝ \land {vol}^{} (B) \in ℝ))$
35	33 34	ax-mp	$⊢ \forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to \forall k \in y (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)$
36	35	imim1i	$⊢ (\forall k \in y (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B)) \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))$
37		simprl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)$
38		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ B$
39		nfcv	$⊢ \underline{Ⅎ} k ℝ$
40	38 39	nfss	$⊢ Ⅎ k ⦋ m / k ⦌ B \subseteq ℝ$
41		nfcv	$⊢ \underline{Ⅎ} k {vol}^{*}$
42	41 38	nffv	$⊢ \underline{Ⅎ} k {vol}^{*} (⦋ m / k ⦌ B)$
43	42	nfel1	$⊢ Ⅎ k {vol}^{*} (⦋ m / k ⦌ B) \in ℝ$
44	40 43	nfan	$⊢ Ⅎ k (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ m / k ⦌ B) \in ℝ)$
45		csbeq1a	$⊢ k = m \to B = ⦋ m / k ⦌ B$
46	45	sseq1d	$⊢ k = m \to (B \subseteq ℝ \leftrightarrow ⦋ m / k ⦌ B \subseteq ℝ)$
47	45	fveq2d	$⊢ k = m \to {vol}^{} (B) = {vol}^{} (⦋ m / k ⦌ B)$
48	47	eleq1d	$⊢ k = m \to ({vol}^{} (B) \in ℝ \leftrightarrow {vol}^{} (⦋ m / k ⦌ B) \in ℝ)$
49	46 48	anbi12d	$⊢ k = m \to ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \leftrightarrow (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ m / k ⦌ B) \in ℝ))$
50	44 49	rspc	$⊢ m \in (y \cup \{z\}) \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ m / k ⦌ B) \in ℝ))$
51	37 50	mpan9	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \land m \in (y \cup \{z\})) \to (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ m / k ⦌ B) \in ℝ)$
52	51	simpld	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \land m \in (y \cup \{z\})) \to ⦋ m / k ⦌ B \subseteq ℝ$
53	52	ralrimiva	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to \forall m \in (y \cup \{z\}) ⦋ m / k ⦌ B \subseteq ℝ$
54		iunss	$⊢ ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B \subseteq ℝ \leftrightarrow \forall m \in (y \cup \{z\}) ⦋ m / k ⦌ B \subseteq ℝ$
55	53 54	sylibr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B \subseteq ℝ$
56		iunss1	$⊢ y \subseteq y \cup \{z\} \to ⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B$
57	33 56	ax-mp	$⊢ ⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B$
58	57 55	sstrid	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to ⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ℝ$
59		simpll	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to y \in Fin$
60		elun1	$⊢ m \in y \to m \in (y \cup \{z\})$
61	51	simprd	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \land m \in (y \cup \{z\})) \to {vol}^{} (⦋ m / k ⦌ B) \in ℝ$
62	60 61	sylan2	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \land m \in y) \to {vol}^{} (⦋ m / k ⦌ B) \in ℝ$
63	59 62	fsumrecl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) \in ℝ$
64		simprr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B)$
65		nfcv	$⊢ \underline{Ⅎ} m B$
66	65 38 45	cbviun	$⊢ ⋃_{k \in y} B = ⋃_{m \in y} ⦋ m / k ⦌ B$
67	66	fveq2i	$⊢ {vol}^{} (⋃_{k \in y} B) = {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B)$
68		nfcv	$⊢ \underline{Ⅎ} m {vol}^{*} (B)$
69	68 42 47	cbvsumi	$⊢ \sum_{k \in y} {vol}^{} (B) = \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B)$
70	64 67 69	3brtr3g	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \leq \sum_{m \in y} {vol}^{*} (⦋ m / k ⦌ B)$
71		ovollecl	$⊢ (⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ℝ \land \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) \in ℝ \land {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \leq \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B)) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \in ℝ$
72	58 63 70 71	syl3anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \in ℝ$
73		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
74		vsnid	$⊢ z \in \{z\}$
75	73 74	sselii	$⊢ z \in (y \cup \{z\})$
76		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ B$
77	76 39	nfss	$⊢ Ⅎ k ⦋ z / k ⦌ B \subseteq ℝ$
78	41 76	nffv	$⊢ \underline{Ⅎ} k {vol}^{*} (⦋ z / k ⦌ B)$
79	78	nfel1	$⊢ Ⅎ k {vol}^{*} (⦋ z / k ⦌ B) \in ℝ$
80	77 79	nfan	$⊢ Ⅎ k (⦋ z / k ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ z / k ⦌ B) \in ℝ)$
81		csbeq1a	$⊢ k = z \to B = ⦋ z / k ⦌ B$
82	81	sseq1d	$⊢ k = z \to (B \subseteq ℝ \leftrightarrow ⦋ z / k ⦌ B \subseteq ℝ)$
83	81	fveq2d	$⊢ k = z \to {vol}^{} (B) = {vol}^{} (⦋ z / k ⦌ B)$
84	83	eleq1d	$⊢ k = z \to ({vol}^{} (B) \in ℝ \leftrightarrow {vol}^{} (⦋ z / k ⦌ B) \in ℝ)$
85	82 84	anbi12d	$⊢ k = z \to ((B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \leftrightarrow (⦋ z / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ z / k ⦌ B) \in ℝ))$
86	80 85	rspc	$⊢ z \in (y \cup \{z\}) \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to (⦋ z / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ z / k ⦌ B) \in ℝ))$
87	75 37 86	mpsyl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to (⦋ z / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ z / k ⦌ B) \in ℝ)$
88	87	simprd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⦋ z / k ⦌ B) \in ℝ$
89	72 88	readdcld	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{*} (⦋ z / k ⦌ B) \in ℝ$
90		iunxun	$⊢ ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B = ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⋃_{m \in \{z\}} ⦋ m / k ⦌ B$
91		vex	$⊢ z \in V$
92		csbeq1	$⊢ m = z \to ⦋ m / k ⦌ B = ⦋ z / k ⦌ B$
93	91 92	iunxsn	$⊢ ⋃_{m \in \{z\}} ⦋ m / k ⦌ B = ⦋ z / k ⦌ B$
94	93	uneq2i	$⊢ ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⋃_{m \in \{z\}} ⦋ m / k ⦌ B = ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B$
95	90 94	eqtri	$⊢ ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B = ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B$
96	95	fveq2i	$⊢ {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) = {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B)$
97		ovolun	$⊢ ((⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \in ℝ) \land (⦋ z / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ z / k ⦌ B) \in ℝ)) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B) \leq {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{*} (⦋ z / k ⦌ B)$
98	58 72 87 97	syl21anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B) \leq {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B)$
99	96 98	eqbrtrid	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) \leq {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B)$
100		ovollecl	$⊢ (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B) \in ℝ \land {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) \leq {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B)) \to {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) \in ℝ$
101	55 89 99 100	syl3anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) \in ℝ$
102		snfi	$⊢ \{z\} \in Fin$
103		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
104	102 103	mpan2	$⊢ y \in Fin \to y \cup \{z\} \in Fin$
105	104	ad2antrr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to y \cup \{z\} \in Fin$
106	105 61	fsumrecl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \sum_{m \in y \cup \{z\}} {vol}^{} (⦋ m / k ⦌ B) \in ℝ$
107	72 63 88 70	leadd1dd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B) \leq \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) + {vol}^{*} (⦋ z / k ⦌ B)$
108		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to \neg z \in y$
109		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
110	108 109	sylibr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to y \cap \{z\} = \emptyset$
111		eqidd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{*} (B))) \to y \cup \{z\} = y \cup \{z\}$
112	61	recnd	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \land m \in (y \cup \{z\})) \to {vol}^{} (⦋ m / k ⦌ B) \in ℂ$
113	110 111 105 112	fsumsplit	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \sum_{m \in y \cup \{z\}} {vol}^{} (⦋ m / k ⦌ B) = \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) + \sum_{m \in \{z\}} {vol}^{} (⦋ m / k ⦌ B)$
114	88	recnd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⦋ z / k ⦌ B) \in ℂ$
115	92	fveq2d	$⊢ m = z \to {vol}^{} (⦋ m / k ⦌ B) = {vol}^{} (⦋ z / k ⦌ B)$
116	115	sumsn	$⊢ (z \in V \land {vol}^{} (⦋ z / k ⦌ B) \in ℂ) \to \sum_{m \in \{z\}} {vol}^{} (⦋ m / k ⦌ B) = {vol}^{*} (⦋ z / k ⦌ B)$
117	91 114 116	sylancr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \sum_{m \in \{z\}} {vol}^{} (⦋ m / k ⦌ B) = {vol}^{*} (⦋ z / k ⦌ B)$
118	117	oveq2d	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) + \sum_{m \in \{z\}} {vol}^{} (⦋ m / k ⦌ B) = \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) + {vol}^{*} (⦋ z / k ⦌ B)$
119	113 118	eqtrd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to \sum_{m \in y \cup \{z\}} {vol}^{} (⦋ m / k ⦌ B) = \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B)$
120	107 119	breqtrrd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) + {vol}^{} (⦋ z / k ⦌ B) \leq \sum_{m \in y \cup \{z\}} {vol}^{} (⦋ m / k ⦌ B)$
121	101 89 106 99 120	letrd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) \leq \sum_{m \in y \cup \{z\}} {vol}^{*} (⦋ m / k ⦌ B)$
122	65 38 45	cbviun	$⊢ ⋃_{k \in y \cup \{z\}} B = ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B$
123	122	fveq2i	$⊢ {vol}^{} (⋃_{k \in y \cup \{z\}} B) = {vol}^{} (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B)$
124	68 42 47	cbvsumi	$⊢ \sum_{k \in y \cup \{z\}} {vol}^{} (B) = \sum_{m \in y \cup \{z\}} {vol}^{} (⦋ m / k ⦌ B)$
125	121 123 124	3brtr4g	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \land {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B))) \to {vol}^{} (⋃_{k \in y \cup \{z\}} B) \leq \sum_{k \in y \cup \{z\}} {vol}^{*} (B)$
126	125	exp32	$⊢ (y \in Fin \land \neg z \in y) \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to ({vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B) \to {vol}^{} (⋃_{k \in y \cup \{z\}} B) \leq \sum_{k \in y \cup \{z\}} {vol}^{*} (B)))$
127	126	a2d	$⊢ (y \in Fin \land \neg z \in y) \to ((\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B)) \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y \cup \{z\}} B) \leq \sum_{k \in y \cup \{z\}} {vol}^{} (B)))$
128	36 127	syl5	$⊢ (y \in Fin \land \neg z \in y) \to ((\forall k \in y (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y} B) \leq \sum_{k \in y} {vol}^{} (B)) \to (\forall k \in (y \cup \{z\}) (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in y \cup \{z\}} B) \leq \sum_{k \in y \cup \{z\}} {vol}^{} (B)))$
129	6 12 18 24 32 128	findcard2s	$⊢ A \in Fin \to (\forall k \in A (B \subseteq ℝ \land {vol}^{} (B) \in ℝ) \to {vol}^{} (⋃_{k \in A} B) \leq \sum_{k \in A} {vol}^{*} (B))$
130	129	imp	$⊢ (A \in Fin \land \forall k \in A (B \subseteq ℝ \land {vol}^{} (B) \in ℝ)) \to {vol}^{} (⋃_{k \in A} B) \leq \sum_{k \in A} {vol}^{*} (B)$

Metamath Proof Explorer

Theorem ovolfiniun

Proof