omeunile

Description: The outer measure of the union of a countable set is the less than or equal to the extended sum of the outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omeunile.o	$⊢ φ \to O \in OutMeas$
	omeunile.x	$⊢ X = ⋃ dom O$
	omeunile.y	$⊢ φ \to Y \subseteq 𝒫 X$
	omeunile.ct	$⊢ φ \to Y ≼ ω$
Assertion	omeunile	$⊢ φ \to O (⋃ Y) \leq sum^({O ↾}_{Y})$

Proof

Step	Hyp	Ref	Expression
1		omeunile.o	$⊢ φ \to O \in OutMeas$
2		omeunile.x	$⊢ X = ⋃ dom O$
3		omeunile.y	$⊢ φ \to Y \subseteq 𝒫 X$
4		omeunile.ct	$⊢ φ \to Y ≼ ω$
5	1 2	unidmex	$⊢ φ \to X \in V$
6	5	pwexd	$⊢ φ \to 𝒫 X \in V$
7		ssexg	$⊢ (Y \subseteq 𝒫 X \land 𝒫 X \in V) \to Y \in V$
8	3 6 7	syl2anc	$⊢ φ \to Y \in V$
9		elpwg	$⊢ Y \in V \to (Y \in 𝒫 𝒫 X \leftrightarrow Y \subseteq 𝒫 X)$
10	8 9	syl	$⊢ φ \to (Y \in 𝒫 𝒫 X \leftrightarrow Y \subseteq 𝒫 X)$
11	3 10	mpbird	$⊢ φ \to Y \in 𝒫 𝒫 X$
12		omedm	$⊢ O \in OutMeas \to dom O = 𝒫 ⋃ dom O$
13	1 12	syl	$⊢ φ \to dom O = 𝒫 ⋃ dom O$
14	2	pweqi	$⊢ 𝒫 X = 𝒫 ⋃ dom O$
15	14	eqcomi	$⊢ 𝒫 ⋃ dom O = 𝒫 X$
16	15	a1i	$⊢ φ \to 𝒫 ⋃ dom O = 𝒫 X$
17	13 16	eqtr2d	$⊢ φ \to 𝒫 X = dom O$
18	17	pweqd	$⊢ φ \to 𝒫 𝒫 X = 𝒫 dom O$
19	11 18	eleqtrd	$⊢ φ \to Y \in 𝒫 dom O$
20		isome	$⊢ O \in OutMeas \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall x \in 𝒫 y O (x) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))))$
21	1 20	syl	$⊢ φ \to (O \in OutMeas \leftrightarrow ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall x \in 𝒫 y O (x) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))))$
22	1 21	mpbid	$⊢ φ \to ((((O : dom O ⟶ [0, +∞] \land dom O = 𝒫 ⋃ dom O) \land O (\emptyset) = 0) \land \forall y \in 𝒫 ⋃ dom O \forall x \in 𝒫 y O (x) \leq O (y)) \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y})))$
23	22	simprd	$⊢ φ \to \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))$
24		breq1	$⊢ y = Y \to (y ≼ ω \leftrightarrow Y ≼ ω)$
25		unieq	$⊢ y = Y \to ⋃ y = ⋃ Y$
26	25	fveq2d	$⊢ y = Y \to O (⋃ y) = O (⋃ Y)$
27		reseq2	$⊢ y = Y \to {O ↾}_{y} = {O ↾}_{Y}$
28	27	fveq2d	$⊢ y = Y \to sum^({O ↾}_{y}) = sum^({O ↾}_{Y})$
29	26 28	breq12d	$⊢ y = Y \to (O (⋃ y) \leq sum^({O ↾}_{y}) \leftrightarrow O (⋃ Y) \leq sum^({O ↾}_{Y}))$
30	24 29	imbi12d	$⊢ y = Y \to ((y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y})) \leftrightarrow (Y ≼ ω \to O (⋃ Y) \leq sum^({O ↾}_{Y})))$
31	30	rspcva	$⊢ (Y \in 𝒫 dom O \land \forall y \in 𝒫 dom O (y ≼ ω \to O (⋃ y) \leq sum^({O ↾}_{y}))) \to (Y ≼ ω \to O (⋃ Y) \leq sum^({O ↾}_{Y}))$
32	19 23 31	syl2anc	$⊢ φ \to (Y ≼ ω \to O (⋃ Y) \leq sum^({O ↾}_{Y}))$
33	4 32	mpd	$⊢ φ \to O (⋃ Y) \leq sum^({O ↾}_{Y})$

Metamath Proof Explorer

Theorem omeunile

Proof