isomenndlem

Description: O is sub-additive w.r.t. countable indexed union, implies that O is sub-additive w.r.t. countable union. Thus, the definition of Outer Measure can be given using an indexed union. Definition 113A of Fremlin1 p. 19 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	isomenndlem.o	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$
	isomenndlem.o0	$⊢ φ \to O (\emptyset) = 0$
	isomenndlem.y	$⊢ φ \to Y \subseteq 𝒫 X$
	isomenndlem.subadd	$⊢ (φ \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))$
	isomenndlem.b	$⊢ φ \to B \subseteq ℕ$
	isomenndlem.f	$⊢ φ \to F : B \underset{1-1 onto}{⟶} Y$
	isomenndlem.a	$⊢ A = (n \in ℕ ⟼ if (n \in B, F (n), \emptyset))$
Assertion	isomenndlem	$⊢ φ \to O (⋃ Y) \leq sum^({O ↾}_{Y})$

Proof

Step	Hyp	Ref	Expression
1		isomenndlem.o	$⊢ φ \to O : 𝒫 X ⟶ [0, +∞]$
2		isomenndlem.o0	$⊢ φ \to O (\emptyset) = 0$
3		isomenndlem.y	$⊢ φ \to Y \subseteq 𝒫 X$
4		isomenndlem.subadd	$⊢ (φ \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))$
5		isomenndlem.b	$⊢ φ \to B \subseteq ℕ$
6		isomenndlem.f	$⊢ φ \to F : B \underset{1-1 onto}{⟶} Y$
7		isomenndlem.a	$⊢ A = (n \in ℕ ⟼ if (n \in B, F (n), \emptyset))$
8		id	$⊢ φ \to φ$
9		iftrue	$⊢ n \in B \to if (n \in B, F (n), \emptyset) = F (n)$
10	9	adantl	$⊢ (φ \land n \in B) \to if (n \in B, F (n), \emptyset) = F (n)$
11		f1of	$⊢ F : B \underset{1-1 onto}{⟶} Y \to F : B ⟶ Y$
12	6 11	syl	$⊢ φ \to F : B ⟶ Y$
13		ssun1	$⊢ Y \subseteq Y \cup \{\emptyset\}$
14	13	a1i	$⊢ φ \to Y \subseteq Y \cup \{\emptyset\}$
15	12 14	fssd	$⊢ φ \to F : B ⟶ Y \cup \{\emptyset\}$
16	15	ffvelrnda	$⊢ (φ \land n \in B) \to F (n) \in (Y \cup \{\emptyset\})$
17	10 16	eqeltrd	$⊢ (φ \land n \in B) \to if (n \in B, F (n), \emptyset) \in (Y \cup \{\emptyset\})$
18	17	adantlr	$⊢ ((φ \land n \in ℕ) \land n \in B) \to if (n \in B, F (n), \emptyset) \in (Y \cup \{\emptyset\})$
19		iffalse	$⊢ \neg n \in B \to if (n \in B, F (n), \emptyset) = \emptyset$
20	19	adantl	$⊢ (φ \land \neg n \in B) \to if (n \in B, F (n), \emptyset) = \emptyset$
21		0ex	$⊢ \emptyset \in V$
22	21	snid	$⊢ \emptyset \in \{\emptyset\}$
23		elun2	$⊢ \emptyset \in \{\emptyset\} \to \emptyset \in (Y \cup \{\emptyset\})$
24	22 23	ax-mp	$⊢ \emptyset \in (Y \cup \{\emptyset\})$
25	24	a1i	$⊢ (φ \land \neg n \in B) \to \emptyset \in (Y \cup \{\emptyset\})$
26	20 25	eqeltrd	$⊢ (φ \land \neg n \in B) \to if (n \in B, F (n), \emptyset) \in (Y \cup \{\emptyset\})$
27	26	adantlr	$⊢ ((φ \land n \in ℕ) \land \neg n \in B) \to if (n \in B, F (n), \emptyset) \in (Y \cup \{\emptyset\})$
28	18 27	pm2.61dan	$⊢ (φ \land n \in ℕ) \to if (n \in B, F (n), \emptyset) \in (Y \cup \{\emptyset\})$
29	28 7	fmptd	$⊢ φ \to A : ℕ ⟶ Y \cup \{\emptyset\}$
30		0elpw	$⊢ \emptyset \in 𝒫 X$
31		snssi	$⊢ \emptyset \in 𝒫 X \to \{\emptyset\} \subseteq 𝒫 X$
32	30 31	ax-mp	$⊢ \{\emptyset\} \subseteq 𝒫 X$
33	32	a1i	$⊢ φ \to \{\emptyset\} \subseteq 𝒫 X$
34	3 33	unssd	$⊢ φ \to Y \cup \{\emptyset\} \subseteq 𝒫 X$
35	29 34	fssd	$⊢ φ \to A : ℕ ⟶ 𝒫 X$
36		nnex	$⊢ ℕ \in V$
37	36	mptex	$⊢ (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) \in V$
38	7 37	eqeltri	$⊢ A \in V$
39		feq1	$⊢ a = A \to (a : ℕ ⟶ 𝒫 X \leftrightarrow A : ℕ ⟶ 𝒫 X)$
40	39	anbi2d	$⊢ a = A \to ((φ \land a : ℕ ⟶ 𝒫 X) \leftrightarrow (φ \land A : ℕ ⟶ 𝒫 X))$
41		fveq1	$⊢ a = A \to a (n) = A (n)$
42	41	iuneq2d	$⊢ a = A \to ⋃_{n \in ℕ} a (n) = ⋃_{n \in ℕ} A (n)$
43	42	fveq2d	$⊢ a = A \to O (⋃_{n \in ℕ} a (n)) = O (⋃_{n \in ℕ} A (n))$
44		simpl	$⊢ (a = A \land n \in ℕ) \to a = A$
45	44	fveq1d	$⊢ (a = A \land n \in ℕ) \to a (n) = A (n)$
46	45	fveq2d	$⊢ (a = A \land n \in ℕ) \to O (a (n)) = O (A (n))$
47	46	mpteq2dva	$⊢ a = A \to (n \in ℕ ⟼ O (a (n))) = (n \in ℕ ⟼ O (A (n)))$
48	47	fveq2d	$⊢ a = A \to sum^((n \in ℕ ⟼ O (a (n)))) = sum^((n \in ℕ ⟼ O (A (n))))$
49	43 48	breq12d	$⊢ a = A \to (O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n)))) \leftrightarrow O (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ O (A (n)))))$
50	40 49	imbi12d	$⊢ a = A \to (((φ \land a : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} a (n)) \leq sum^((n \in ℕ ⟼ O (a (n))))) \leftrightarrow ((φ \land A : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ O (A (n))))))$
51	38 50 4	vtocl	$⊢ (φ \land A : ℕ ⟶ 𝒫 X) \to O (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ O (A (n))))$
52	8 35 51	syl2anc	$⊢ φ \to O (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ O (A (n))))$
53	12	ad2antrr	$⊢ ((φ \land B = ℕ) \land n \in ℕ) \to F : B ⟶ Y$
54		simpr	$⊢ (B = ℕ \land n \in ℕ) \to n \in ℕ$
55		id	$⊢ B = ℕ \to B = ℕ$
56	55	eqcomd	$⊢ B = ℕ \to ℕ = B$
57	56	adantr	$⊢ (B = ℕ \land n \in ℕ) \to ℕ = B$
58	54 57	eleqtrd	$⊢ (B = ℕ \land n \in ℕ) \to n \in B$
59	58	adantll	$⊢ ((φ \land B = ℕ) \land n \in ℕ) \to n \in B$
60	53 59	ffvelrnd	$⊢ ((φ \land B = ℕ) \land n \in ℕ) \to F (n) \in Y$
61		eqid	$⊢ (n \in ℕ ⟼ F (n)) = (n \in ℕ ⟼ F (n))$
62	60 61	fmptd	$⊢ (φ \land B = ℕ) \to (n \in ℕ ⟼ F (n)) : ℕ ⟶ Y$
63	7	a1i	$⊢ B = ℕ \to A = (n \in ℕ ⟼ if (n \in B, F (n), \emptyset))$
64	58	iftrued	$⊢ (B = ℕ \land n \in ℕ) \to if (n \in B, F (n), \emptyset) = F (n)$
65	64	mpteq2dva	$⊢ B = ℕ \to (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) = (n \in ℕ ⟼ F (n))$
66	63 65	eqtrd	$⊢ B = ℕ \to A = (n \in ℕ ⟼ F (n))$
67	66	feq1d	$⊢ B = ℕ \to (A : ℕ ⟶ Y \leftrightarrow (n \in ℕ ⟼ F (n)) : ℕ ⟶ Y)$
68	67	adantl	$⊢ (φ \land B = ℕ) \to (A : ℕ ⟶ Y \leftrightarrow (n \in ℕ ⟼ F (n)) : ℕ ⟶ Y)$
69	62 68	mpbird	$⊢ (φ \land B = ℕ) \to A : ℕ ⟶ Y$
70		f1ofo	$⊢ F : B \underset{1-1 onto}{⟶} Y \to F : B \underset{onto}{⟶} Y$
71	6 70	syl	$⊢ φ \to F : B \underset{onto}{⟶} Y$
72		dffo3	$⊢ F : B \underset{onto}{⟶} Y \leftrightarrow (F : B ⟶ Y \land \forall y \in Y \exists n \in B y = F (n))$
73	71 72	sylib	$⊢ φ \to (F : B ⟶ Y \land \forall y \in Y \exists n \in B y = F (n))$
74	73	simprd	$⊢ φ \to \forall y \in Y \exists n \in B y = F (n)$
75	74	adantr	$⊢ (φ \land y \in Y) \to \forall y \in Y \exists n \in B y = F (n)$
76		simpr	$⊢ (φ \land y \in Y) \to y \in Y$
77		rspa	$⊢ (\forall y \in Y \exists n \in B y = F (n) \land y \in Y) \to \exists n \in B y = F (n)$
78	75 76 77	syl2anc	$⊢ (φ \land y \in Y) \to \exists n \in B y = F (n)$
79	78	adantlr	$⊢ ((φ \land B = ℕ) \land y \in Y) \to \exists n \in B y = F (n)$
80		nfv	$⊢ Ⅎ n (φ \land B = ℕ)$
81		nfre1	$⊢ Ⅎ n \exists n \in ℕ y = A (n)$
82		simpr	$⊢ (B = ℕ \land n \in B) \to n \in B$
83		simpl	$⊢ (B = ℕ \land n \in B) \to B = ℕ$
84	82 83	eleqtrd	$⊢ (B = ℕ \land n \in B) \to n \in ℕ$
85	84	adantll	$⊢ ((φ \land B = ℕ) \land n \in B) \to n \in ℕ$
86	85	3adant3	$⊢ ((φ \land B = ℕ) \land n \in B \land y = F (n)) \to n \in ℕ$
87	63	fveq1d	$⊢ B = ℕ \to A (n) = (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) (n)$
88	87	3ad2ant1	$⊢ (B = ℕ \land n \in B \land y = F (n)) \to A (n) = (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) (n)$
89		fvex	$⊢ F (n) \in V$
90	89 21	ifex	$⊢ if (n \in B, F (n), \emptyset) \in V$
91	90	a1i	$⊢ (B = ℕ \land n \in B) \to if (n \in B, F (n), \emptyset) \in V$
92		eqid	$⊢ (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) = (n \in ℕ ⟼ if (n \in B, F (n), \emptyset))$
93	92	fvmpt2	$⊢ (n \in ℕ \land if (n \in B, F (n), \emptyset) \in V) \to (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) (n) = if (n \in B, F (n), \emptyset)$
94	84 91 93	syl2anc	$⊢ (B = ℕ \land n \in B) \to (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) (n) = if (n \in B, F (n), \emptyset)$
95	9	adantl	$⊢ (B = ℕ \land n \in B) \to if (n \in B, F (n), \emptyset) = F (n)$
96	94 95	eqtrd	$⊢ (B = ℕ \land n \in B) \to (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) (n) = F (n)$
97	96	3adant3	$⊢ (B = ℕ \land n \in B \land y = F (n)) \to (n \in ℕ ⟼ if (n \in B, F (n), \emptyset)) (n) = F (n)$
98		id	$⊢ y = F (n) \to y = F (n)$
99	98	eqcomd	$⊢ y = F (n) \to F (n) = y$
100	99	3ad2ant3	$⊢ (B = ℕ \land n \in B \land y = F (n)) \to F (n) = y$
101	88 97 100	3eqtrrd	$⊢ (B = ℕ \land n \in B \land y = F (n)) \to y = A (n)$
102	101	3adant1l	$⊢ ((φ \land B = ℕ) \land n \in B \land y = F (n)) \to y = A (n)$
103		rspe	$⊢ (n \in ℕ \land y = A (n)) \to \exists n \in ℕ y = A (n)$
104	86 102 103	syl2anc	$⊢ ((φ \land B = ℕ) \land n \in B \land y = F (n)) \to \exists n \in ℕ y = A (n)$
105	104	3exp	$⊢ (φ \land B = ℕ) \to (n \in B \to (y = F (n) \to \exists n \in ℕ y = A (n)))$
106	80 81 105	rexlimd	$⊢ (φ \land B = ℕ) \to (\exists n \in B y = F (n) \to \exists n \in ℕ y = A (n))$
107	106	adantr	$⊢ ((φ \land B = ℕ) \land y \in Y) \to (\exists n \in B y = F (n) \to \exists n \in ℕ y = A (n))$
108	79 107	mpd	$⊢ ((φ \land B = ℕ) \land y \in Y) \to \exists n \in ℕ y = A (n)$
109	108	ralrimiva	$⊢ (φ \land B = ℕ) \to \forall y \in Y \exists n \in ℕ y = A (n)$
110	69 109	jca	$⊢ (φ \land B = ℕ) \to (A : ℕ ⟶ Y \land \forall y \in Y \exists n \in ℕ y = A (n))$
111		dffo3	$⊢ A : ℕ \underset{onto}{⟶} Y \leftrightarrow (A : ℕ ⟶ Y \land \forall y \in Y \exists n \in ℕ y = A (n))$
112	110 111	sylibr	$⊢ (φ \land B = ℕ) \to A : ℕ \underset{onto}{⟶} Y$
113		founiiun	$⊢ A : ℕ \underset{onto}{⟶} Y \to ⋃ Y = ⋃_{n \in ℕ} A (n)$
114	112 113	syl	$⊢ (φ \land B = ℕ) \to ⋃ Y = ⋃_{n \in ℕ} A (n)$
115		uniun	$⊢ ⋃ (Y \cup \{\emptyset\}) = ⋃ Y \cup ⋃ \{\emptyset\}$
116	21	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
117	116	uneq2i	$⊢ ⋃ Y \cup ⋃ \{\emptyset\} = ⋃ Y \cup \emptyset$
118		un0	$⊢ ⋃ Y \cup \emptyset = ⋃ Y$
119	115 117 118	3eqtrri	$⊢ ⋃ Y = ⋃ (Y \cup \{\emptyset\})$
120	119	a1i	$⊢ (φ \land \neg B = ℕ) \to ⋃ Y = ⋃ (Y \cup \{\emptyset\})$
121	29	adantr	$⊢ (φ \land \neg B = ℕ) \to A : ℕ ⟶ Y \cup \{\emptyset\}$
122		nfv	$⊢ Ⅎ n ((φ \land \neg B = ℕ) \land y = \emptyset)$
123	5	adantr	$⊢ (φ \land \neg B = ℕ) \to B \subseteq ℕ$
124	55	necon3bi	$⊢ \neg B = ℕ \to B \neq ℕ$
125	124	adantl	$⊢ (φ \land \neg B = ℕ) \to B \neq ℕ$
126	123 125	jca	$⊢ (φ \land \neg B = ℕ) \to (B \subseteq ℕ \land B \neq ℕ)$
127		df-pss	$⊢ B \subset ℕ \leftrightarrow (B \subseteq ℕ \land B \neq ℕ)$
128	126 127	sylibr	$⊢ (φ \land \neg B = ℕ) \to B \subset ℕ$
129		pssnel	$⊢ B \subset ℕ \to \exists n (n \in ℕ \land \neg n \in B)$
130	128 129	syl	$⊢ (φ \land \neg B = ℕ) \to \exists n (n \in ℕ \land \neg n \in B)$
131	130	adantr	$⊢ ((φ \land \neg B = ℕ) \land y = \emptyset) \to \exists n (n \in ℕ \land \neg n \in B)$
132		simprl	$⊢ ((φ \land y = \emptyset) \land (n \in ℕ \land \neg n \in B)) \to n \in ℕ$
133		simprl	$⊢ (φ \land (n \in ℕ \land \neg n \in B)) \to n \in ℕ$
134	90	a1i	$⊢ (φ \land (n \in ℕ \land \neg n \in B)) \to if (n \in B, F (n), \emptyset) \in V$
135	7	fvmpt2	$⊢ (n \in ℕ \land if (n \in B, F (n), \emptyset) \in V) \to A (n) = if (n \in B, F (n), \emptyset)$
136	133 134 135	syl2anc	$⊢ (φ \land (n \in ℕ \land \neg n \in B)) \to A (n) = if (n \in B, F (n), \emptyset)$
137	136	adantlr	$⊢ ((φ \land y = \emptyset) \land (n \in ℕ \land \neg n \in B)) \to A (n) = if (n \in B, F (n), \emptyset)$
138	19	ad2antll	$⊢ ((φ \land y = \emptyset) \land (n \in ℕ \land \neg n \in B)) \to if (n \in B, F (n), \emptyset) = \emptyset$
139		id	$⊢ y = \emptyset \to y = \emptyset$
140	139	eqcomd	$⊢ y = \emptyset \to \emptyset = y$
141	140	ad2antlr	$⊢ ((φ \land y = \emptyset) \land (n \in ℕ \land \neg n \in B)) \to \emptyset = y$
142	137 138 141	3eqtrrd	$⊢ ((φ \land y = \emptyset) \land (n \in ℕ \land \neg n \in B)) \to y = A (n)$
143	132 142 103	syl2anc	$⊢ ((φ \land y = \emptyset) \land (n \in ℕ \land \neg n \in B)) \to \exists n \in ℕ y = A (n)$
144	143	ex	$⊢ (φ \land y = \emptyset) \to ((n \in ℕ \land \neg n \in B) \to \exists n \in ℕ y = A (n))$
145	144	adantlr	$⊢ ((φ \land \neg B = ℕ) \land y = \emptyset) \to ((n \in ℕ \land \neg n \in B) \to \exists n \in ℕ y = A (n))$
146	122 81 131 145	exlimimdd	$⊢ ((φ \land \neg B = ℕ) \land y = \emptyset) \to \exists n \in ℕ y = A (n)$
147	146	adantlr	$⊢ (((φ \land \neg B = ℕ) \land y \in (Y \cup \{\emptyset\})) \land y = \emptyset) \to \exists n \in ℕ y = A (n)$
148		simplll	$⊢ (((φ \land \neg B = ℕ) \land y \in (Y \cup \{\emptyset\})) \land \neg y = \emptyset) \to φ$
149		simpl	$⊢ (y \in (Y \cup \{\emptyset\}) \land \neg y = \emptyset) \to y \in (Y \cup \{\emptyset\})$
150		elsni	$⊢ y \in \{\emptyset\} \to y = \emptyset$
151	150	con3i	$⊢ \neg y = \emptyset \to \neg y \in \{\emptyset\}$
152	151	adantl	$⊢ (y \in (Y \cup \{\emptyset\}) \land \neg y = \emptyset) \to \neg y \in \{\emptyset\}$
153		elunnel2	$⊢ (y \in (Y \cup \{\emptyset\}) \land \neg y \in \{\emptyset\}) \to y \in Y$
154	149 152 153	syl2anc	$⊢ (y \in (Y \cup \{\emptyset\}) \land \neg y = \emptyset) \to y \in Y$
155	154	adantll	$⊢ (((φ \land \neg B = ℕ) \land y \in (Y \cup \{\emptyset\})) \land \neg y = \emptyset) \to y \in Y$
156	71	adantr	$⊢ (φ \land y \in Y) \to F : B \underset{onto}{⟶} Y$
157		foelrni	$⊢ (F : B \underset{onto}{⟶} Y \land y \in Y) \to \exists n \in B F (n) = y$
158	156 76 157	syl2anc	$⊢ (φ \land y \in Y) \to \exists n \in B F (n) = y$
159		nfv	$⊢ Ⅎ n (φ \land y \in Y)$
160	5	sselda	$⊢ (φ \land n \in B) \to n \in ℕ$
161	160	3adant3	$⊢ (φ \land n \in B \land F (n) = y) \to n \in ℕ$
162	160 90 135	sylancl	$⊢ (φ \land n \in B) \to A (n) = if (n \in B, F (n), \emptyset)$
163	162 10	eqtrd	$⊢ (φ \land n \in B) \to A (n) = F (n)$
164	163	3adant3	$⊢ (φ \land n \in B \land F (n) = y) \to A (n) = F (n)$
165		simp3	$⊢ (φ \land n \in B \land F (n) = y) \to F (n) = y$
166	164 165	eqtr2d	$⊢ (φ \land n \in B \land F (n) = y) \to y = A (n)$
167	161 166 103	syl2anc	$⊢ (φ \land n \in B \land F (n) = y) \to \exists n \in ℕ y = A (n)$
168	167	3exp	$⊢ φ \to (n \in B \to (F (n) = y \to \exists n \in ℕ y = A (n)))$
169	168	adantr	$⊢ (φ \land y \in Y) \to (n \in B \to (F (n) = y \to \exists n \in ℕ y = A (n)))$
170	159 81 169	rexlimd	$⊢ (φ \land y \in Y) \to (\exists n \in B F (n) = y \to \exists n \in ℕ y = A (n))$
171	158 170	mpd	$⊢ (φ \land y \in Y) \to \exists n \in ℕ y = A (n)$
172	148 155 171	syl2anc	$⊢ (((φ \land \neg B = ℕ) \land y \in (Y \cup \{\emptyset\})) \land \neg y = \emptyset) \to \exists n \in ℕ y = A (n)$
173	147 172	pm2.61dan	$⊢ ((φ \land \neg B = ℕ) \land y \in (Y \cup \{\emptyset\})) \to \exists n \in ℕ y = A (n)$
174	173	ralrimiva	$⊢ (φ \land \neg B = ℕ) \to \forall y \in (Y \cup \{\emptyset\}) \exists n \in ℕ y = A (n)$
175	121 174	jca	$⊢ (φ \land \neg B = ℕ) \to (A : ℕ ⟶ Y \cup \{\emptyset\} \land \forall y \in (Y \cup \{\emptyset\}) \exists n \in ℕ y = A (n))$
176		dffo3	$⊢ A : ℕ \underset{onto}{⟶} Y \cup \{\emptyset\} \leftrightarrow (A : ℕ ⟶ Y \cup \{\emptyset\} \land \forall y \in (Y \cup \{\emptyset\}) \exists n \in ℕ y = A (n))$
177	175 176	sylibr	$⊢ (φ \land \neg B = ℕ) \to A : ℕ \underset{onto}{⟶} Y \cup \{\emptyset\}$
178		founiiun	$⊢ A : ℕ \underset{onto}{⟶} Y \cup \{\emptyset\} \to ⋃ (Y \cup \{\emptyset\}) = ⋃_{n \in ℕ} A (n)$
179	177 178	syl	$⊢ (φ \land \neg B = ℕ) \to ⋃ (Y \cup \{\emptyset\}) = ⋃_{n \in ℕ} A (n)$
180	120 179	eqtrd	$⊢ (φ \land \neg B = ℕ) \to ⋃ Y = ⋃_{n \in ℕ} A (n)$
181	114 180	pm2.61dan	$⊢ φ \to ⋃ Y = ⋃_{n \in ℕ} A (n)$
182	181	fveq2d	$⊢ φ \to O (⋃ Y) = O (⋃_{n \in ℕ} A (n))$
183		uncom	$⊢ (ℕ ∖ B) \cup B = B \cup (ℕ ∖ B)$
184	183	a1i	$⊢ φ \to (ℕ ∖ B) \cup B = B \cup (ℕ ∖ B)$
185		undif	$⊢ B \subseteq ℕ \leftrightarrow B \cup (ℕ ∖ B) = ℕ$
186	5 185	sylib	$⊢ φ \to B \cup (ℕ ∖ B) = ℕ$
187	184 186	eqtrd	$⊢ φ \to (ℕ ∖ B) \cup B = ℕ$
188	187	eqcomd	$⊢ φ \to ℕ = (ℕ ∖ B) \cup B$
189	188	mpteq1d	$⊢ φ \to (n \in ℕ ⟼ O (A (n))) = (n \in ((ℕ ∖ B) \cup B) ⟼ O (A (n)))$
190	189	fveq2d	$⊢ φ \to sum^((n \in ℕ ⟼ O (A (n)))) = sum^((n \in ((ℕ ∖ B) \cup B) ⟼ O (A (n))))$
191		nfv	$⊢ Ⅎ n φ$
192		difexg	$⊢ ℕ \in V \to ℕ ∖ B \in V$
193	36 192	ax-mp	$⊢ ℕ ∖ B \in V$
194	193	a1i	$⊢ φ \to ℕ ∖ B \in V$
195	36	a1i	$⊢ φ \to ℕ \in V$
196	195 5	ssexd	$⊢ φ \to B \in V$
197		incom	$⊢ (ℕ ∖ B) \cap B = B \cap (ℕ ∖ B)$
198		disjdif	$⊢ B \cap (ℕ ∖ B) = \emptyset$
199	197 198	eqtri	$⊢ (ℕ ∖ B) \cap B = \emptyset$
200	199	a1i	$⊢ φ \to (ℕ ∖ B) \cap B = \emptyset$
201		simpl	$⊢ (φ \land n \in (ℕ ∖ B)) \to φ$
202		eldifi	$⊢ n \in (ℕ ∖ B) \to n \in ℕ$
203	202	adantl	$⊢ (φ \land n \in (ℕ ∖ B)) \to n \in ℕ$
204	1	adantr	$⊢ (φ \land n \in ℕ) \to O : 𝒫 X ⟶ [0, +∞]$
205	35	ffvelrnda	$⊢ (φ \land n \in ℕ) \to A (n) \in 𝒫 X$
206	204 205	ffvelrnd	$⊢ (φ \land n \in ℕ) \to O (A (n)) \in [0, +∞]$
207	201 203 206	syl2anc	$⊢ (φ \land n \in (ℕ ∖ B)) \to O (A (n)) \in [0, +∞]$
208	160 206	syldan	$⊢ (φ \land n \in B) \to O (A (n)) \in [0, +∞]$
209	191 194 196 200 207 208	sge0splitmpt	$⊢ φ \to sum^((n \in ((ℕ ∖ B) \cup B) ⟼ O (A (n)))) = sum^((n \in (ℕ ∖ B) ⟼ O (A (n)))) +_{𝑒} sum^((n \in B ⟼ O (A (n))))$
210		eqid	$⊢ (n \in B ⟼ O (A (n))) = (n \in B ⟼ O (A (n)))$
211	208 210	fmptd	$⊢ φ \to (n \in B ⟼ O (A (n))) : B ⟶ [0, +∞]$
212	196 211	sge0xrcl	$⊢ φ \to sum^((n \in B ⟼ O (A (n)))) \in ℝ^{*}$
213	212	xaddid2d	$⊢ φ \to 0 +_{𝑒} sum^((n \in B ⟼ O (A (n)))) = sum^((n \in B ⟼ O (A (n))))$
214	90	a1i	$⊢ (φ \land n \in (ℕ ∖ B)) \to if (n \in B, F (n), \emptyset) \in V$
215	203 214 135	syl2anc	$⊢ (φ \land n \in (ℕ ∖ B)) \to A (n) = if (n \in B, F (n), \emptyset)$
216		eldifn	$⊢ n \in (ℕ ∖ B) \to \neg n \in B$
217	216	adantl	$⊢ (φ \land n \in (ℕ ∖ B)) \to \neg n \in B$
218	217	iffalsed	$⊢ (φ \land n \in (ℕ ∖ B)) \to if (n \in B, F (n), \emptyset) = \emptyset$
219	215 218	eqtrd	$⊢ (φ \land n \in (ℕ ∖ B)) \to A (n) = \emptyset$
220	219	fveq2d	$⊢ (φ \land n \in (ℕ ∖ B)) \to O (A (n)) = O (\emptyset)$
221	201 2	syl	$⊢ (φ \land n \in (ℕ ∖ B)) \to O (\emptyset) = 0$
222	220 221	eqtrd	$⊢ (φ \land n \in (ℕ ∖ B)) \to O (A (n)) = 0$
223	222	mpteq2dva	$⊢ φ \to (n \in (ℕ ∖ B) ⟼ O (A (n))) = (n \in (ℕ ∖ B) ⟼ 0)$
224	223	fveq2d	$⊢ φ \to sum^((n \in (ℕ ∖ B) ⟼ O (A (n)))) = sum^((n \in (ℕ ∖ B) ⟼ 0))$
225	191 194	sge0z	$⊢ φ \to sum^((n \in (ℕ ∖ B) ⟼ 0)) = 0$
226	224 225	eqtrd	$⊢ φ \to sum^((n \in (ℕ ∖ B) ⟼ O (A (n)))) = 0$
227	226	oveq1d	$⊢ φ \to sum^((n \in (ℕ ∖ B) ⟼ O (A (n)))) +_{𝑒} sum^((n \in B ⟼ O (A (n)))) = 0 +_{𝑒} sum^((n \in B ⟼ O (A (n))))$
228	1 3	feqresmpt	$⊢ φ \to {O ↾}_{Y} = (y \in Y ⟼ O (y))$
229	228	fveq2d	$⊢ φ \to sum^({O ↾}_{Y}) = sum^((y \in Y ⟼ O (y)))$
230		nfv	$⊢ Ⅎ y φ$
231		fveq2	$⊢ y = A (n) \to O (y) = O (A (n))$
232	163	eqcomd	$⊢ (φ \land n \in B) \to F (n) = A (n)$
233	1	adantr	$⊢ (φ \land y \in Y) \to O : 𝒫 X ⟶ [0, +∞]$
234	3	sselda	$⊢ (φ \land y \in Y) \to y \in 𝒫 X$
235	233 234	ffvelrnd	$⊢ (φ \land y \in Y) \to O (y) \in [0, +∞]$
236	230 191 231 196 6 232 235	sge0f1o	$⊢ φ \to sum^((y \in Y ⟼ O (y))) = sum^((n \in B ⟼ O (A (n))))$
237		eqidd	$⊢ φ \to sum^((n \in B ⟼ O (A (n)))) = sum^((n \in B ⟼ O (A (n))))$
238	229 236 237	3eqtrd	$⊢ φ \to sum^({O ↾}_{Y}) = sum^((n \in B ⟼ O (A (n))))$
239	213 227 238	3eqtr4d	$⊢ φ \to sum^((n \in (ℕ ∖ B) ⟼ O (A (n)))) +_{𝑒} sum^((n \in B ⟼ O (A (n)))) = sum^({O ↾}_{Y})$
240	190 209 239	3eqtrrd	$⊢ φ \to sum^({O ↾}_{Y}) = sum^((n \in ℕ ⟼ O (A (n))))$
241	182 240	breq12d	$⊢ φ \to (O (⋃ Y) \leq sum^({O ↾}_{Y}) \leftrightarrow O (⋃_{n \in ℕ} A (n)) \leq sum^((n \in ℕ ⟼ O (A (n)))))$
242	52 241	mpbird	$⊢ φ \to O (⋃ Y) \leq sum^({O ↾}_{Y})$

Metamath Proof Explorer

Theorem isomenndlem

Proof