volfiniun

Description: The volume of a disjoint finite union of measurable sets is the sum of the measures. (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 11-Dec-2016)

		Ref	Expression
	Assertion	volfiniun	$⊢ (A \in Fin \land \forall k \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in A}{Disj} B) \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B)$

Proof

Step	Hyp	Ref	Expression
1		raleq	$⊢ w = \emptyset \to (\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \leftrightarrow \forall k \in \emptyset (B \in dom vol \land vol (B) \in ℝ))$
2		disjeq1	$⊢ w = \emptyset \to (\underset{k \in w}{Disj} B \leftrightarrow \underset{k \in \emptyset}{Disj} B)$
3	1 2	anbi12d	$⊢ w = \emptyset \to ((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \leftrightarrow (\forall k \in \emptyset (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in \emptyset}{Disj} B))$
4		iuneq1	$⊢ w = \emptyset \to ⋃_{k \in w} B = ⋃_{k \in \emptyset} B$
5	4	fveq2d	$⊢ w = \emptyset \to vol (⋃_{k \in w} B) = vol (⋃_{k \in \emptyset} B)$
6		sumeq1	$⊢ w = \emptyset \to \sum_{k \in w} vol (B) = \sum_{k \in \emptyset} vol (B)$
7	5 6	eqeq12d	$⊢ w = \emptyset \to (vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B) \leftrightarrow vol (⋃_{k \in \emptyset} B) = \sum_{k \in \emptyset} vol (B))$
8	3 7	imbi12d	$⊢ w = \emptyset \to (((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \to vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B)) \leftrightarrow ((\forall k \in \emptyset (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in \emptyset}{Disj} B) \to vol (⋃_{k \in \emptyset} B) = \sum_{k \in \emptyset} vol (B)))$
9		raleq	$⊢ w = y \to (\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \leftrightarrow \forall k \in y (B \in dom vol \land vol (B) \in ℝ))$
10		disjeq1	$⊢ w = y \to (\underset{k \in w}{Disj} B \leftrightarrow \underset{k \in y}{Disj} B)$
11	9 10	anbi12d	$⊢ w = y \to ((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \leftrightarrow (\forall k \in y (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y}{Disj} B))$
12		iuneq1	$⊢ w = y \to ⋃_{k \in w} B = ⋃_{k \in y} B$
13	12	fveq2d	$⊢ w = y \to vol (⋃_{k \in w} B) = vol (⋃_{k \in y} B)$
14		sumeq1	$⊢ w = y \to \sum_{k \in w} vol (B) = \sum_{k \in y} vol (B)$
15	13 14	eqeq12d	$⊢ w = y \to (vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B) \leftrightarrow vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B))$
16	11 15	imbi12d	$⊢ w = y \to (((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \to vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B)) \leftrightarrow ((\forall k \in y (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y}{Disj} B) \to vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B)))$
17		raleq	$⊢ w = y \cup \{z\} \to (\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \leftrightarrow \forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ))$
18		disjeq1	$⊢ w = y \cup \{z\} \to (\underset{k \in w}{Disj} B \leftrightarrow \underset{k \in y \cup \{z\}}{Disj} B)$
19	17 18	anbi12d	$⊢ w = y \cup \{z\} \to ((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \leftrightarrow (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B))$
20		iuneq1	$⊢ w = y \cup \{z\} \to ⋃_{k \in w} B = ⋃_{k \in y \cup \{z\}} B$
21	20	fveq2d	$⊢ w = y \cup \{z\} \to vol (⋃_{k \in w} B) = vol (⋃_{k \in y \cup \{z\}} B)$
22		sumeq1	$⊢ w = y \cup \{z\} \to \sum_{k \in w} vol (B) = \sum_{k \in y \cup \{z\}} vol (B)$
23	21 22	eqeq12d	$⊢ w = y \cup \{z\} \to (vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B) \leftrightarrow vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B))$
24	19 23	imbi12d	$⊢ w = y \cup \{z\} \to (((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \to vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B)) \leftrightarrow ((\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B)))$
25		raleq	$⊢ w = A \to (\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \leftrightarrow \forall k \in A (B \in dom vol \land vol (B) \in ℝ))$
26		disjeq1	$⊢ w = A \to (\underset{k \in w}{Disj} B \leftrightarrow \underset{k \in A}{Disj} B)$
27	25 26	anbi12d	$⊢ w = A \to ((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \leftrightarrow (\forall k \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in A}{Disj} B))$
28		iuneq1	$⊢ w = A \to ⋃_{k \in w} B = ⋃_{k \in A} B$
29	28	fveq2d	$⊢ w = A \to vol (⋃_{k \in w} B) = vol (⋃_{k \in A} B)$
30		sumeq1	$⊢ w = A \to \sum_{k \in w} vol (B) = \sum_{k \in A} vol (B)$
31	29 30	eqeq12d	$⊢ w = A \to (vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B) \leftrightarrow vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B))$
32	27 31	imbi12d	$⊢ w = A \to (((\forall k \in w (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in w}{Disj} B) \to vol (⋃_{k \in w} B) = \sum_{k \in w} vol (B)) \leftrightarrow ((\forall k \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in A}{Disj} B) \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B)))$
33		0mbl	$⊢ \emptyset \in dom vol$
34		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
35	33 34	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
36		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
37	35 36	eqtri	$⊢ vol (\emptyset) = 0$
38		0iun	$⊢ ⋃_{k \in \emptyset} B = \emptyset$
39	38	fveq2i	$⊢ vol (⋃_{k \in \emptyset} B) = vol (\emptyset)$
40		sum0	$⊢ \sum_{k \in \emptyset} vol (B) = 0$
41	37 39 40	3eqtr4i	$⊢ vol (⋃_{k \in \emptyset} B) = \sum_{k \in \emptyset} vol (B)$
42	41	a1i	$⊢ (\forall k \in \emptyset (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in \emptyset}{Disj} B) \to vol (⋃_{k \in \emptyset} B) = \sum_{k \in \emptyset} vol (B)$
43		ssun1	$⊢ y \subseteq y \cup \{z\}$
44		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \to \forall k \in y (B \in dom vol \land vol (B) \in ℝ))$
45	43 44	ax-mp	$⊢ \forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \to \forall k \in y (B \in dom vol \land vol (B) \in ℝ)$
46		disjss1	$⊢ y \subseteq y \cup \{z\} \to (\underset{k \in y \cup \{z\}}{Disj} B \to \underset{k \in y}{Disj} B)$
47	43 46	ax-mp	$⊢ \underset{k \in y \cup \{z\}}{Disj} B \to \underset{k \in y}{Disj} B$
48	45 47	anim12i	$⊢ (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to (\forall k \in y (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y}{Disj} B)$
49	48	imim1i	$⊢ ((\forall k \in y (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y}{Disj} B) \to vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B)) \to ((\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B))$
50		oveq1	$⊢ vol (⋃_{m \in y} ⦋ m / k ⦌ B) = \sum_{m \in y} vol (⦋ m / k ⦌ B) \to vol (⋃_{m \in y} ⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B) = \sum_{m \in y} vol (⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B)$
51		iunxun	$⊢ ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B = ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⋃_{m \in \{z\}} ⦋ m / k ⦌ B$
52		vex	$⊢ z \in V$
53		csbeq1	$⊢ m = z \to ⦋ m / k ⦌ B = ⦋ z / k ⦌ B$
54	52 53	iunxsn	$⊢ ⋃_{m \in \{z\}} ⦋ m / k ⦌ B = ⦋ z / k ⦌ B$
55	54	uneq2i	$⊢ ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⋃_{m \in \{z\}} ⦋ m / k ⦌ B = ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B$
56	51 55	eqtri	$⊢ ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B = ⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B$
57	56	fveq2i	$⊢ vol (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) = vol (⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B)$
58		nfcv	$⊢ \underline{Ⅎ} m B$
59		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ B$
60		csbeq1a	$⊢ k = m \to B = ⦋ m / k ⦌ B$
61	58 59 60	cbviun	$⊢ ⋃_{k \in y} B = ⋃_{m \in y} ⦋ m / k ⦌ B$
62		simpll	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to y \in Fin$
63		simprl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ)$
64		simpl	$⊢ (B \in dom vol \land vol (B) \in ℝ) \to B \in dom vol$
65	64	ralimi	$⊢ \forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \to \forall k \in (y \cup \{z\}) B \in dom vol$
66	63 65	syl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall k \in (y \cup \{z\}) B \in dom vol$
67		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall k \in (y \cup \{z\}) B \in dom vol \to \forall k \in y B \in dom vol)$
68	43 66 67	mpsyl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall k \in y B \in dom vol$
69		finiunmbl	$⊢ (y \in Fin \land \forall k \in y B \in dom vol) \to ⋃_{k \in y} B \in dom vol$
70	62 68 69	syl2anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to ⋃_{k \in y} B \in dom vol$
71	61 70	eqeltrrid	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to ⋃_{m \in y} ⦋ m / k ⦌ B \in dom vol$
72		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
73		vsnid	$⊢ z \in \{z\}$
74	72 73	sselii	$⊢ z \in (y \cup \{z\})$
75		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ z / k ⦌ B$
76	75	nfel1	$⊢ Ⅎ k ⦋ z / k ⦌ B \in dom vol$
77		nfcv	$⊢ \underline{Ⅎ} k vol$
78	77 75	nffv	$⊢ \underline{Ⅎ} k vol (⦋ z / k ⦌ B)$
79	78	nfel1	$⊢ Ⅎ k vol (⦋ z / k ⦌ B) \in ℝ$
80	76 79	nfan	$⊢ Ⅎ k (⦋ z / k ⦌ B \in dom vol \land vol (⦋ z / k ⦌ B) \in ℝ)$
81		csbeq1a	$⊢ k = z \to B = ⦋ z / k ⦌ B$
82	81	eleq1d	$⊢ k = z \to (B \in dom vol \leftrightarrow ⦋ z / k ⦌ B \in dom vol)$
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 \in dom vol \land vol (B) \in ℝ) \leftrightarrow (⦋ z / k ⦌ B \in dom vol \land vol (⦋ z / k ⦌ B) \in ℝ))$
86	80 85	rspc	$⊢ z \in (y \cup \{z\}) \to (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \to (⦋ z / k ⦌ B \in dom vol \land vol (⦋ z / k ⦌ B) \in ℝ))$
87	74 63 86	mpsyl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (⦋ z / k ⦌ B \in dom vol \land vol (⦋ z / k ⦌ B) \in ℝ)$
88	87	simpld	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to ⦋ z / k ⦌ B \in dom vol$
89		simplr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \neg z \in y$
90		elin	$⊢ w \in (⋃_{m \in y} ⦋ m / k ⦌ B \cap ⦋ z / k ⦌ B) \leftrightarrow (w \in ⋃_{m \in y} ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)$
91		eliun	$⊢ w \in ⋃_{m \in y} ⦋ m / k ⦌ B \leftrightarrow \exists m \in y w \in ⦋ m / k ⦌ B$
92		simplrr	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to \underset{k \in y \cup \{z\}}{Disj} B$
93		nfcv	$⊢ \underline{Ⅎ} n B$
94		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ n / k ⦌ B$
95		csbeq1a	$⊢ k = n \to B = ⦋ n / k ⦌ B$
96	93 94 95	cbvdisj	$⊢ \underset{k \in y \cup \{z\}}{Disj} B \leftrightarrow \underset{n \in y \cup \{z\}}{Disj} ⦋ n / k ⦌ B$
97	92 96	sylib	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to \underset{n \in y \cup \{z\}}{Disj} ⦋ n / k ⦌ B$
98		simpr1	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to m \in y$
99		elun1	$⊢ m \in y \to m \in (y \cup \{z\})$
100	98 99	syl	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to m \in (y \cup \{z\})$
101	74	a1i	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to z \in (y \cup \{z\})$
102		simpr2	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to w \in ⦋ m / k ⦌ B$
103		simpr3	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to w \in ⦋ z / k ⦌ B$
104		csbeq1	$⊢ n = m \to ⦋ n / k ⦌ B = ⦋ m / k ⦌ B$
105		csbeq1	$⊢ n = z \to ⦋ n / k ⦌ B = ⦋ z / k ⦌ B$
106	104 105	disji	$⊢ (\underset{n \in y \cup \{z\}}{Disj} ⦋ n / k ⦌ B \land (m \in (y \cup \{z\}) \land z \in (y \cup \{z\})) \land (w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to m = z$
107	97 100 101 102 103 106	syl122anc	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to m = z$
108	107 98	eqeltrrd	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land (m \in y \land w \in ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B)) \to z \in y$
109	108	3exp2	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (m \in y \to (w \in ⦋ m / k ⦌ B \to (w \in ⦋ z / k ⦌ B \to z \in y)))$
110	109	rexlimdv	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (\exists m \in y w \in ⦋ m / k ⦌ B \to (w \in ⦋ z / k ⦌ B \to z \in y))$
111	91 110	syl5bi	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (w \in ⋃_{m \in y} ⦋ m / k ⦌ B \to (w \in ⦋ z / k ⦌ B \to z \in y))$
112	111	impd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to ((w \in ⋃_{m \in y} ⦋ m / k ⦌ B \land w \in ⦋ z / k ⦌ B) \to z \in y)$
113	90 112	syl5bi	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (w \in (⋃_{m \in y} ⦋ m / k ⦌ B \cap ⦋ z / k ⦌ B) \to z \in y)$
114	89 113	mtod	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \neg w \in (⋃_{m \in y} ⦋ m / k ⦌ B \cap ⦋ z / k ⦌ B)$
115	114	eq0rdv	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to ⋃_{m \in y} ⦋ m / k ⦌ B \cap ⦋ z / k ⦌ B = \emptyset$
116		mblvol	$⊢ ⋃_{m \in y} ⦋ m / k ⦌ B \in dom vol \to vol (⋃_{m \in y} ⦋ m / k ⦌ B) = {vol}^{*} (⋃_{m \in y} ⦋ m / k ⦌ B)$
117	71 116	syl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to vol (⋃_{m \in y} ⦋ m / k ⦌ B) = {vol}^{*} (⋃_{m \in y} ⦋ m / k ⦌ B)$
118		nfv	$⊢ Ⅎ m (B \in dom vol \land vol (B) \in ℝ)$
119	59	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ B \in dom vol$
120	77 59	nffv	$⊢ \underline{Ⅎ} k vol (⦋ m / k ⦌ B)$
121	120	nfel1	$⊢ Ⅎ k vol (⦋ m / k ⦌ B) \in ℝ$
122	119 121	nfan	$⊢ Ⅎ k (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ)$
123	60	eleq1d	$⊢ k = m \to (B \in dom vol \leftrightarrow ⦋ m / k ⦌ B \in dom vol)$
124	60	fveq2d	$⊢ k = m \to vol (B) = vol (⦋ m / k ⦌ B)$
125	124	eleq1d	$⊢ k = m \to (vol (B) \in ℝ \leftrightarrow vol (⦋ m / k ⦌ B) \in ℝ)$
126	123 125	anbi12d	$⊢ k = m \to ((B \in dom vol \land vol (B) \in ℝ) \leftrightarrow (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ))$
127	118 122 126	cbvralw	$⊢ \forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \leftrightarrow \forall m \in (y \cup \{z\}) (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ)$
128	63 127	sylib	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall m \in (y \cup \{z\}) (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ)$
129	128	r19.21bi	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in (y \cup \{z\})) \to (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ)$
130	129	simpld	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in (y \cup \{z\})) \to ⦋ m / k ⦌ B \in dom vol$
131		mblss	$⊢ ⦋ m / k ⦌ B \in dom vol \to ⦋ m / k ⦌ B \subseteq ℝ$
132	130 131	syl	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in (y \cup \{z\})) \to ⦋ m / k ⦌ B \subseteq ℝ$
133	99 132	sylan2	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in y) \to ⦋ m / k ⦌ B \subseteq ℝ$
134	133	ralrimiva	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall m \in y ⦋ m / k ⦌ B \subseteq ℝ$
135		iunss	$⊢ ⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ℝ \leftrightarrow \forall m \in y ⦋ m / k ⦌ B \subseteq ℝ$
136	134 135	sylibr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to ⋃_{m \in y} ⦋ m / k ⦌ B \subseteq ℝ$
137		mblvol	$⊢ ⦋ m / k ⦌ B \in dom vol \to vol (⦋ m / k ⦌ B) = {vol}^{*} (⦋ m / k ⦌ B)$
138	137	eleq1d	$⊢ ⦋ m / k ⦌ B \in dom vol \to (vol (⦋ m / k ⦌ B) \in ℝ \leftrightarrow {vol}^{*} (⦋ m / k ⦌ B) \in ℝ)$
139	138	biimpa	$⊢ (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ) \to {vol}^{*} (⦋ m / k ⦌ B) \in ℝ$
140	129 139	syl	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in (y \cup \{z\})) \to {vol}^{*} (⦋ m / k ⦌ B) \in ℝ$
141	99 140	sylan2	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in y) \to {vol}^{*} (⦋ m / k ⦌ B) \in ℝ$
142	62 141	fsumrecl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \sum_{m \in y} {vol}^{*} (⦋ m / k ⦌ B) \in ℝ$
143	131	adantr	$⊢ (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ) \to ⦋ m / k ⦌ B \subseteq ℝ$
144	143 139	jca	$⊢ (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ) \to (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ m / k ⦌ B) \in ℝ)$
145	144	ralimi	$⊢ \forall m \in (y \cup \{z\}) (⦋ m / k ⦌ B \in dom vol \land vol (⦋ m / k ⦌ B) \in ℝ) \to \forall m \in (y \cup \{z\}) (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ m / k ⦌ B) \in ℝ)$
146	128 145	syl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall m \in (y \cup \{z\}) (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ m / k ⦌ B) \in ℝ)$
147		ssralv	$⊢ y \subseteq y \cup \{z\} \to (\forall m \in (y \cup \{z\}) (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ m / k ⦌ B) \in ℝ) \to \forall m \in y (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ m / k ⦌ B) \in ℝ))$
148	43 146 147	mpsyl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \forall m \in y (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{*} (⦋ m / k ⦌ B) \in ℝ)$
149		ovolfiniun	$⊢ (y \in Fin \land \forall m \in y (⦋ m / k ⦌ B \subseteq ℝ \land {vol}^{} (⦋ m / k ⦌ B) \in ℝ)) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \leq \sum_{m \in y} {vol}^{*} (⦋ m / k ⦌ B)$
150	62 148 149	syl2anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to {vol}^{} (⋃_{m \in y} ⦋ m / k ⦌ B) \leq \sum_{m \in y} {vol}^{} (⦋ m / k ⦌ B)$
151		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 ℝ$
152	136 142 150 151	syl3anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to {vol}^{*} (⋃_{m \in y} ⦋ m / k ⦌ B) \in ℝ$
153	117 152	eqeltrd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to vol (⋃_{m \in y} ⦋ m / k ⦌ B) \in ℝ$
154	87	simprd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to vol (⦋ z / k ⦌ B) \in ℝ$
155		volun	$⊢ ((⋃_{m \in y} ⦋ m / k ⦌ B \in dom vol \land ⦋ z / k ⦌ B \in dom vol \land ⋃_{m \in y} ⦋ m / k ⦌ B \cap ⦋ z / k ⦌ B = \emptyset) \land (vol (⋃_{m \in y} ⦋ m / k ⦌ B) \in ℝ \land vol (⦋ z / k ⦌ B) \in ℝ)) \to vol (⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B) = vol (⋃_{m \in y} ⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B)$
156	71 88 115 153 154 155	syl32anc	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to vol (⋃_{m \in y} ⦋ m / k ⦌ B \cup ⦋ z / k ⦌ B) = vol (⋃_{m \in y} ⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B)$
157	57 156	syl5eq	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to vol (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) = vol (⋃_{m \in y} ⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B)$
158		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
159	89 158	sylibr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to y \cap \{z\} = \emptyset$
160		eqidd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to y \cup \{z\} = y \cup \{z\}$
161		snfi	$⊢ \{z\} \in Fin$
162		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
163	62 161 162	sylancl	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to y \cup \{z\} \in Fin$
164	129	simprd	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in (y \cup \{z\})) \to vol (⦋ m / k ⦌ B) \in ℝ$
165	164	recnd	$⊢ (((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \land m \in (y \cup \{z\})) \to vol (⦋ m / k ⦌ B) \in ℂ$
166	159 160 163 165	fsumsplit	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} 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)$
167	154	recnd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to vol (⦋ z / k ⦌ B) \in ℂ$
168	53	fveq2d	$⊢ m = z \to vol (⦋ m / k ⦌ B) = vol (⦋ z / k ⦌ B)$
169	168	sumsn	$⊢ (z \in V \land vol (⦋ z / k ⦌ B) \in ℂ) \to \sum_{m \in \{z\}} vol (⦋ m / k ⦌ B) = vol (⦋ z / k ⦌ B)$
170	52 167 169	sylancr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \sum_{m \in \{z\}} vol (⦋ m / k ⦌ B) = vol (⦋ z / k ⦌ B)$
171	170	oveq2d	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} 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)$
172	166 171	eqtrd	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to \sum_{m \in y \cup \{z\}} vol (⦋ m / k ⦌ B) = \sum_{m \in y} vol (⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B)$
173	157 172	eqeq12d	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (vol (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) = \sum_{m \in y \cup \{z\}} vol (⦋ m / k ⦌ B) \leftrightarrow vol (⋃_{m \in y} ⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B) = \sum_{m \in y} vol (⦋ m / k ⦌ B) + vol (⦋ z / k ⦌ B))$
174	50 173	syl5ibr	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (vol (⋃_{m \in y} ⦋ m / k ⦌ B) = \sum_{m \in y} vol (⦋ m / k ⦌ B) \to vol (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) = \sum_{m \in y \cup \{z\}} vol (⦋ m / k ⦌ B))$
175	61	fveq2i	$⊢ vol (⋃_{k \in y} B) = vol (⋃_{m \in y} ⦋ m / k ⦌ B)$
176		nfcv	$⊢ \underline{Ⅎ} m vol (B)$
177	176 120 124	cbvsumi	$⊢ \sum_{k \in y} vol (B) = \sum_{m \in y} vol (⦋ m / k ⦌ B)$
178	175 177	eqeq12i	$⊢ vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B) \leftrightarrow vol (⋃_{m \in y} ⦋ m / k ⦌ B) = \sum_{m \in y} vol (⦋ m / k ⦌ B)$
179	58 59 60	cbviun	$⊢ ⋃_{k \in y \cup \{z\}} B = ⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B$
180	179	fveq2i	$⊢ vol (⋃_{k \in y \cup \{z\}} B) = vol (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B)$
181	176 120 124	cbvsumi	$⊢ \sum_{k \in y \cup \{z\}} vol (B) = \sum_{m \in y \cup \{z\}} vol (⦋ m / k ⦌ B)$
182	180 181	eqeq12i	$⊢ vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B) \leftrightarrow vol (⋃_{m \in y \cup \{z\}} ⦋ m / k ⦌ B) = \sum_{m \in y \cup \{z\}} vol (⦋ m / k ⦌ B)$
183	174 178 182	3imtr4g	$⊢ ((y \in Fin \land \neg z \in y) \land (\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B)) \to (vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B) \to vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B))$
184	183	ex	$⊢ (y \in Fin \land \neg z \in y) \to ((\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to (vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B) \to vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B)))$
185	184	a2d	$⊢ (y \in Fin \land \neg z \in y) \to (((\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B)) \to ((\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B)))$
186	49 185	syl5	$⊢ (y \in Fin \land \neg z \in y) \to (((\forall k \in y (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y}{Disj} B) \to vol (⋃_{k \in y} B) = \sum_{k \in y} vol (B)) \to ((\forall k \in (y \cup \{z\}) (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in y \cup \{z\}}{Disj} B) \to vol (⋃_{k \in y \cup \{z\}} B) = \sum_{k \in y \cup \{z\}} vol (B)))$
187	8 16 24 32 42 186	findcard2s	$⊢ A \in Fin \to ((\forall k \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in A}{Disj} B) \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B))$
188	187	3impib	$⊢ (A \in Fin \land \forall k \in A (B \in dom vol \land vol (B) \in ℝ) \land \underset{k \in A}{Disj} B) \to vol (⋃_{k \in A} B) = \sum_{k \in A} vol (B)$

Metamath Proof Explorer

Theorem volfiniun

Proof