Metamath Proof Explorer

Theorem omeiunlempt

Description: The outer measure of the indexed 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 omeiunlempt.nph ⊢ Ⅎ 𝑛 𝜑
omeiunlempt.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
omeiunlempt.x ⊢ 𝑋 = ∪ dom 𝑂
omeiunlempt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
omeiunlempt.e ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐸 ⊆ 𝑋 )
Assertion omeiunlempt ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 𝐸 ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ 𝐸 ) ) ) )

Proof

Step Hyp Ref Expression
1 omeiunlempt.nph ⊢ Ⅎ 𝑛 𝜑
2 omeiunlempt.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
3 omeiunlempt.x ⊢ 𝑋 = ∪ dom 𝑂
4 omeiunlempt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
5 omeiunlempt.e ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐸 ⊆ 𝑋 )
6 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ 𝑍 ↦ 𝐸 )
7 2 3 unidmex ⊢ ( 𝜑 → 𝑋 ∈ V )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑋 ∈ V )
9 ssexg ⊢ ( ( 𝐸 ⊆ 𝑋 ∧ 𝑋 ∈ V ) → 𝐸 ∈ V )
10 5 8 9 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐸 ∈ V )
11 elpwg ⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝒫 𝑋 ↔ 𝐸 ⊆ 𝑋 ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ∈ 𝒫 𝑋 ↔ 𝐸 ⊆ 𝑋 ) )
13 5 12 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐸 ∈ 𝒫 𝑋 )
14 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) = ( 𝑛 ∈ 𝑍 ↦ 𝐸 )
15 1 13 14 fmptdf ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) : 𝑍 ⟶ 𝒫 𝑋 )
16 1 6 2 3 4 15 omeiunle ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) ) ) )
17 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
18 14 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝐸 ∈ V ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) = 𝐸 )
19 17 10 18 syl2anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) = 𝐸 )
20 19 eqcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝐸 = ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) )
21 1 20 iuneq2df ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 𝐸 = ∪ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 𝐸 ) = ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) )
23 20 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑂 ‘ 𝐸 ) = ( 𝑂 ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) )
24 1 23 mpteq2da ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ 𝐸 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) ) )
25 24 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ 𝐸 ) ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) ) ) )
26 22 25 breq12d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 𝐸 ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ 𝐸 ) ) ) ↔ ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐸 ) ‘ 𝑛 ) ) ) ) ) )
27 16 26 mpbird ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 𝐸 ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ 𝐸 ) ) ) )