Theorem 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	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omeunile.x	⊢ 𝑋 = ∪ dom 𝑂
	omeunile.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝒫 𝑋 )
	omeunile.ct	⊢ ( 𝜑 → 𝑌 ≼ ω )
Assertion	omeunile	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		omeunile.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
2		omeunile.x	⊢ 𝑋 = ∪ dom 𝑂
3		omeunile.y	⊢ ( 𝜑 → 𝑌 ⊆ 𝒫 𝑋 )
4		omeunile.ct	⊢ ( 𝜑 → 𝑌 ≼ ω )
5	1 2	unidmex	⊢ ( 𝜑 → 𝑋 ∈ V )
6	5	pwexd	⊢ ( 𝜑 → 𝒫 𝑋 ∈ V )
7		ssexg	⊢ ( ( 𝑌 ⊆ 𝒫 𝑋 ∧ 𝒫 𝑋 ∈ V ) → 𝑌 ∈ V )
8	3 6 7	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ V )
9		elpwg	⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ 𝑌 ⊆ 𝒫 𝑋 ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝑌 ∈ 𝒫 𝒫 𝑋 ↔ 𝑌 ⊆ 𝒫 𝑋 ) )
11	3 10	mpbird	⊢ ( 𝜑 → 𝑌 ∈ 𝒫 𝒫 𝑋 )
12		omedm	⊢ ( 𝑂 ∈ OutMeas → dom 𝑂 = 𝒫 ∪ dom 𝑂 )
13	1 12	syl	⊢ ( 𝜑 → dom 𝑂 = 𝒫 ∪ dom 𝑂 )
14	2	pweqi	⊢ 𝒫 𝑋 = 𝒫 ∪ dom 𝑂
15	14	eqcomi	⊢ 𝒫 ∪ dom 𝑂 = 𝒫 𝑋
16	15	a1i	⊢ ( 𝜑 → 𝒫 ∪ dom 𝑂 = 𝒫 𝑋 )
17	13 16	eqtr2d	⊢ ( 𝜑 → 𝒫 𝑋 = dom 𝑂 )
18	17	pweqd	⊢ ( 𝜑 → 𝒫 𝒫 𝑋 = 𝒫 dom 𝑂 )
19	11 18	eleqtrd	⊢ ( 𝜑 → 𝑌 ∈ 𝒫 dom 𝑂 )
20		isome	⊢ ( 𝑂 ∈ OutMeas → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑥 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
21	1 20	syl	⊢ ( 𝜑 → ( 𝑂 ∈ OutMeas ↔ ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑥 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) ) )
22	1 21	mpbid	⊢ ( 𝜑 → ( ( ( ( 𝑂 : dom 𝑂 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑂 = 𝒫 ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 ∪ dom 𝑂 ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑂 ‘ 𝑥 ) ≤ ( 𝑂 ‘ 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) )
23	22	simprd	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) )
24		breq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≼ ω ↔ 𝑌 ≼ ω ) )
25		unieq	⊢ ( 𝑦 = 𝑌 → ∪ 𝑦 = ∪ 𝑌 )
26	25	fveq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑂 ‘ ∪ 𝑦 ) = ( 𝑂 ‘ ∪ 𝑌 ) )
27		reseq2	⊢ ( 𝑦 = 𝑌 → ( 𝑂 ↾ 𝑦 ) = ( 𝑂 ↾ 𝑌 ) )
28	27	fveq2d	⊢ ( 𝑦 = 𝑌 → ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) = ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) )
29	26 28	breq12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ↔ ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) ) )
30	24 29	imbi12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ↔ ( 𝑌 ≼ ω → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) ) ) )
31	30	rspcva	⊢ ( ( 𝑌 ∈ 𝒫 dom 𝑂 ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑂 ( 𝑦 ≼ ω → ( 𝑂 ‘ ∪ 𝑦 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑦 ) ) ) ) → ( 𝑌 ≼ ω → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) ) )
32	19 23 31	syl2anc	⊢ ( 𝜑 → ( 𝑌 ≼ ω → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) ) )
33	4 32	mpd	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑌 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ 𝑌 ) ) )