ovnsubadd2lem

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnsubadd2lem.x	$⊢ φ \to X \in Fin$
	ovnsubadd2lem.a	$⊢ φ \to A \subseteq ℝ^{X}$
	ovnsubadd2lem.b	$⊢ φ \to B \subseteq ℝ^{X}$
	ovnsubadd2lem.c	$⊢ C = (n \in ℕ ⟼ if (n = 1, A, if (n = 2, B, \emptyset)))$
Assertion	ovnsubadd2lem	$⊢ φ \to voln* (X) (A \cup B) \leq voln* (X) (A) +_{𝑒} voln* (X) (B)$

Proof

Step	Hyp	Ref	Expression
1		ovnsubadd2lem.x	$⊢ φ \to X \in Fin$
2		ovnsubadd2lem.a	$⊢ φ \to A \subseteq ℝ^{X}$
3		ovnsubadd2lem.b	$⊢ φ \to B \subseteq ℝ^{X}$
4		ovnsubadd2lem.c	$⊢ C = (n \in ℕ ⟼ if (n = 1, A, if (n = 2, B, \emptyset)))$
5		iftrue	$⊢ n = 1 \to if (n = 1, A, if (n = 2, B, \emptyset)) = A$
6	5	adantl	$⊢ (φ \land n = 1) \to if (n = 1, A, if (n = 2, B, \emptyset)) = A$
7		ovexd	$⊢ φ \to ℝ^{X} \in V$
8	7 2	ssexd	$⊢ φ \to A \in V$
9	8 2	elpwd	$⊢ φ \to A \in 𝒫 (ℝ^{X})$
10	9	adantr	$⊢ (φ \land n = 1) \to A \in 𝒫 (ℝ^{X})$
11	6 10	eqeltrd	$⊢ (φ \land n = 1) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
12	11	adantlr	$⊢ ((φ \land n \in ℕ) \land n = 1) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
13		simpl	$⊢ (\neg n = 1 \land n = 2) \to \neg n = 1$
14	13	iffalsed	$⊢ (\neg n = 1 \land n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) = if (n = 2, B, \emptyset)$
15		simpr	$⊢ (\neg n = 1 \land n = 2) \to n = 2$
16	15	iftrued	$⊢ (\neg n = 1 \land n = 2) \to if (n = 2, B, \emptyset) = B$
17	14 16	eqtrd	$⊢ (\neg n = 1 \land n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) = B$
18	17	adantll	$⊢ ((φ \land \neg n = 1) \land n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) = B$
19	7 3	ssexd	$⊢ φ \to B \in V$
20	19 3	elpwd	$⊢ φ \to B \in 𝒫 (ℝ^{X})$
21	20	ad2antrr	$⊢ ((φ \land \neg n = 1) \land n = 2) \to B \in 𝒫 (ℝ^{X})$
22	18 21	eqeltrd	$⊢ ((φ \land \neg n = 1) \land n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
23	22	adantllr	$⊢ (((φ \land n \in ℕ) \land \neg n = 1) \land n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
24		simpl	$⊢ (\neg n = 1 \land \neg n = 2) \to \neg n = 1$
25	24	iffalsed	$⊢ (\neg n = 1 \land \neg n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) = if (n = 2, B, \emptyset)$
26		simpr	$⊢ (\neg n = 1 \land \neg n = 2) \to \neg n = 2$
27	26	iffalsed	$⊢ (\neg n = 1 \land \neg n = 2) \to if (n = 2, B, \emptyset) = \emptyset$
28	25 27	eqtrd	$⊢ (\neg n = 1 \land \neg n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) = \emptyset$
29		0elpw	$⊢ \emptyset \in 𝒫 (ℝ^{X})$
30	29	a1i	$⊢ (\neg n = 1 \land \neg n = 2) \to \emptyset \in 𝒫 (ℝ^{X})$
31	28 30	eqeltrd	$⊢ (\neg n = 1 \land \neg n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
32	31	adantll	$⊢ (((φ \land n \in ℕ) \land \neg n = 1) \land \neg n = 2) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
33	23 32	pm2.61dan	$⊢ ((φ \land n \in ℕ) \land \neg n = 1) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
34	12 33	pm2.61dan	$⊢ (φ \land n \in ℕ) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in 𝒫 (ℝ^{X})$
35	34 4	fmptd	$⊢ φ \to C : ℕ ⟶ 𝒫 (ℝ^{X})$
36	1 35	ovnsubadd	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} C (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (C (n))))$
37		eldifi	$⊢ n \in (ℕ ∖ \{1, 2\}) \to n \in ℕ$
38	37	adantl	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to n \in ℕ$
39		eldifn	$⊢ n \in (ℕ ∖ \{1, 2\}) \to \neg n \in \{1, 2\}$
40		vex	$⊢ n \in V$
41	40	a1i	$⊢ \neg n \in \{1, 2\} \to n \in V$
42		id	$⊢ \neg n \in \{1, 2\} \to \neg n \in \{1, 2\}$
43	41 42	nelpr1	$⊢ \neg n \in \{1, 2\} \to n \neq 1$
44	43	neneqd	$⊢ \neg n \in \{1, 2\} \to \neg n = 1$
45	39 44	syl	$⊢ n \in (ℕ ∖ \{1, 2\}) \to \neg n = 1$
46	41 42	nelpr2	$⊢ \neg n \in \{1, 2\} \to n \neq 2$
47	46	neneqd	$⊢ \neg n \in \{1, 2\} \to \neg n = 2$
48	39 47	syl	$⊢ n \in (ℕ ∖ \{1, 2\}) \to \neg n = 2$
49	45 48 28	syl2anc	$⊢ n \in (ℕ ∖ \{1, 2\}) \to if (n = 1, A, if (n = 2, B, \emptyset)) = \emptyset$
50		0ex	$⊢ \emptyset \in V$
51	50	a1i	$⊢ n \in (ℕ ∖ \{1, 2\}) \to \emptyset \in V$
52	49 51	eqeltrd	$⊢ n \in (ℕ ∖ \{1, 2\}) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in V$
53	52	adantl	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to if (n = 1, A, if (n = 2, B, \emptyset)) \in V$
54	4	fvmpt2	$⊢ (n \in ℕ \land if (n = 1, A, if (n = 2, B, \emptyset)) \in V) \to C (n) = if (n = 1, A, if (n = 2, B, \emptyset))$
55	38 53 54	syl2anc	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to C (n) = if (n = 1, A, if (n = 2, B, \emptyset))$
56	49	adantl	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to if (n = 1, A, if (n = 2, B, \emptyset)) = \emptyset$
57	55 56	eqtrd	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to C (n) = \emptyset$
58	57	ralrimiva	$⊢ φ \to \forall n \in (ℕ ∖ \{1, 2\}) C (n) = \emptyset$
59		nfcv	$⊢ \underline{Ⅎ} n (ℕ ∖ \{1, 2\})$
60	59	iunxdif3	$⊢ \forall n \in (ℕ ∖ \{1, 2\}) C (n) = \emptyset \to ⋃_{n \in ℕ ∖ (ℕ ∖ \{1, 2\})} C (n) = ⋃_{n \in ℕ} C (n)$
61	58 60	syl	$⊢ φ \to ⋃_{n \in ℕ ∖ (ℕ ∖ \{1, 2\})} C (n) = ⋃_{n \in ℕ} C (n)$
62	61	eqcomd	$⊢ φ \to ⋃_{n \in ℕ} C (n) = ⋃_{n \in ℕ ∖ (ℕ ∖ \{1, 2\})} C (n)$
63		1nn	$⊢ 1 \in ℕ$
64		2nn	$⊢ 2 \in ℕ$
65	63 64	pm3.2i	$⊢ (1 \in ℕ \land 2 \in ℕ)$
66		prssi	$⊢ (1 \in ℕ \land 2 \in ℕ) \to \{1, 2\} \subseteq ℕ$
67	65 66	ax-mp	$⊢ \{1, 2\} \subseteq ℕ$
68		dfss4	$⊢ \{1, 2\} \subseteq ℕ \leftrightarrow ℕ ∖ (ℕ ∖ \{1, 2\}) = \{1, 2\}$
69	67 68	mpbi	$⊢ ℕ ∖ (ℕ ∖ \{1, 2\}) = \{1, 2\}$
70		iuneq1	$⊢ ℕ ∖ (ℕ ∖ \{1, 2\}) = \{1, 2\} \to ⋃_{n \in ℕ ∖ (ℕ ∖ \{1, 2\})} C (n) = ⋃_{n \in \{1, 2\}} C (n)$
71	69 70	ax-mp	$⊢ ⋃_{n \in ℕ ∖ (ℕ ∖ \{1, 2\})} C (n) = ⋃_{n \in \{1, 2\}} C (n)$
72	71	a1i	$⊢ φ \to ⋃_{n \in ℕ ∖ (ℕ ∖ \{1, 2\})} C (n) = ⋃_{n \in \{1, 2\}} C (n)$
73		fveq2	$⊢ n = 1 \to C (n) = C (1)$
74		fveq2	$⊢ n = 2 \to C (n) = C (2)$
75	73 74	iunxprg	$⊢ (1 \in ℕ \land 2 \in ℕ) \to ⋃_{n \in \{1, 2\}} C (n) = C (1) \cup C (2)$
76	63 64 75	mp2an	$⊢ ⋃_{n \in \{1, 2\}} C (n) = C (1) \cup C (2)$
77	76	a1i	$⊢ φ \to ⋃_{n \in \{1, 2\}} C (n) = C (1) \cup C (2)$
78	63	a1i	$⊢ φ \to 1 \in ℕ$
79	4 5 78 8	fvmptd3	$⊢ φ \to C (1) = A$
80		id	$⊢ n = 2 \to n = 2$
81		1ne2	$⊢ 1 \neq 2$
82	81	necomi	$⊢ 2 \neq 1$
83	82	a1i	$⊢ n = 2 \to 2 \neq 1$
84	80 83	eqnetrd	$⊢ n = 2 \to n \neq 1$
85	84	neneqd	$⊢ n = 2 \to \neg n = 1$
86	85	iffalsed	$⊢ n = 2 \to if (n = 1, A, if (n = 2, B, \emptyset)) = if (n = 2, B, \emptyset)$
87		iftrue	$⊢ n = 2 \to if (n = 2, B, \emptyset) = B$
88	86 87	eqtrd	$⊢ n = 2 \to if (n = 1, A, if (n = 2, B, \emptyset)) = B$
89	64	a1i	$⊢ φ \to 2 \in ℕ$
90	4 88 89 19	fvmptd3	$⊢ φ \to C (2) = B$
91	79 90	uneq12d	$⊢ φ \to C (1) \cup C (2) = A \cup B$
92		eqidd	$⊢ φ \to A \cup B = A \cup B$
93	77 91 92	3eqtrd	$⊢ φ \to ⋃_{n \in \{1, 2\}} C (n) = A \cup B$
94	62 72 93	3eqtrd	$⊢ φ \to ⋃_{n \in ℕ} C (n) = A \cup B$
95	94	fveq2d	$⊢ φ \to voln* (X) (⋃_{n \in ℕ} C (n)) = voln* (X) (A \cup B)$
96		nfv	$⊢ Ⅎ n φ$
97		nnex	$⊢ ℕ \in V$
98	97	a1i	$⊢ φ \to ℕ \in V$
99	67	a1i	$⊢ φ \to \{1, 2\} \subseteq ℕ$
100	1	adantr	$⊢ (φ \land n \in \{1, 2\}) \to X \in Fin$
101		simpl	$⊢ (φ \land n \in \{1, 2\}) \to φ$
102	99	sselda	$⊢ (φ \land n \in \{1, 2\}) \to n \in ℕ$
103	35	ffvelrnda	$⊢ (φ \land n \in ℕ) \to C (n) \in 𝒫 (ℝ^{X})$
104		elpwi	$⊢ C (n) \in 𝒫 (ℝ^{X}) \to C (n) \subseteq ℝ^{X}$
105	103 104	syl	$⊢ (φ \land n \in ℕ) \to C (n) \subseteq ℝ^{X}$
106	101 102 105	syl2anc	$⊢ (φ \land n \in \{1, 2\}) \to C (n) \subseteq ℝ^{X}$
107	100 106	ovncl	$⊢ (φ \land n \in \{1, 2\}) \to voln* (X) (C (n)) \in [0, +∞]$
108	57	fveq2d	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to voln* (X) (C (n)) = voln* (X) (\emptyset)$
109	1	adantr	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to X \in Fin$
110	109	ovn0	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to voln* (X) (\emptyset) = 0$
111	108 110	eqtrd	$⊢ (φ \land n \in (ℕ ∖ \{1, 2\})) \to voln* (X) (C (n)) = 0$
112	96 98 99 107 111	sge0ss	$⊢ φ \to sum^((n \in \{1, 2\} ⟼ voln* (X) (C (n)))) = sum^((n \in ℕ ⟼ voln* (X) (C (n))))$
113	112	eqcomd	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (C (n)))) = sum^((n \in \{1, 2\} ⟼ voln* (X) (C (n))))$
114	79 2	eqsstrd	$⊢ φ \to C (1) \subseteq ℝ^{X}$
115	1 114	ovncl	$⊢ φ \to voln* (X) (C (1)) \in [0, +∞]$
116	90 3	eqsstrd	$⊢ φ \to C (2) \subseteq ℝ^{X}$
117	1 116	ovncl	$⊢ φ \to voln* (X) (C (2)) \in [0, +∞]$
118		2fveq3	$⊢ n = 1 \to voln* (X) (C (n)) = voln* (X) (C (1))$
119		2fveq3	$⊢ n = 2 \to voln* (X) (C (n)) = voln* (X) (C (2))$
120	81	a1i	$⊢ φ \to 1 \neq 2$
121	78 89 115 117 118 119 120	sge0pr	$⊢ φ \to sum^((n \in \{1, 2\} ⟼ voln* (X) (C (n)))) = voln* (X) (C (1)) +_{𝑒} voln* (X) (C (2))$
122	79	fveq2d	$⊢ φ \to voln* (X) (C (1)) = voln* (X) (A)$
123	90	fveq2d	$⊢ φ \to voln* (X) (C (2)) = voln* (X) (B)$
124	122 123	oveq12d	$⊢ φ \to voln* (X) (C (1)) +_{𝑒} voln* (X) (C (2)) = voln* (X) (A) +_{𝑒} voln* (X) (B)$
125	113 121 124	3eqtrd	$⊢ φ \to sum^((n \in ℕ ⟼ voln* (X) (C (n)))) = voln* (X) (A) +_{𝑒} voln* (X) (B)$
126	95 125	breq12d	$⊢ φ \to (voln* (X) (⋃_{n \in ℕ} C (n)) \leq sum^((n \in ℕ ⟼ voln* (X) (C (n)))) \leftrightarrow voln* (X) (A \cup B) \leq voln* (X) (A) +_{𝑒} voln* (X) (B))$
127	36 126	mpbid	$⊢ φ \to voln* (X) (A \cup B) \leq voln* (X) (A) +_{𝑒} voln* (X) (B)$

Metamath Proof Explorer

Theorem ovnsubadd2lem

Proof