Metamath Proof Explorer

Theorem omeiunle

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 omeiunle.nph ⊢ Ⅎ 𝑛 𝜑
omeiunle.ne ⊢ Ⅎ 𝑛 𝐸
omeiunle.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
omeiunle.x ⊢ 𝑋 = ∪ dom 𝑂
omeiunle.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
omeiunle.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
Assertion omeiunle ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 omeiunle.nph ⊢ Ⅎ 𝑛 𝜑
2 omeiunle.ne ⊢ Ⅎ 𝑛 𝐸
3 omeiunle.o ⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
4 omeiunle.x ⊢ 𝑋 = ∪ dom 𝑂
5 omeiunle.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
6 omeiunle.e ⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
7 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
8 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
9 elpwi ⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
10 8 9 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
11 10 ex ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 ) )
12 1 11 ralrimi ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
13 iunss ⊢ ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
14 12 13 sylibr ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
15 3 4 14 omecl ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
16 7 15 sselid ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
17 6 ffnd ⊢ ( 𝜑 → 𝐸 Fn 𝑍 )
18 5 fvexi ⊢ 𝑍 ∈ V
19 18 a1i ⊢ ( 𝜑 → 𝑍 ∈ V )
20 fnex ⊢ ( ( 𝐸 Fn 𝑍 ∧ 𝑍 ∈ V ) → 𝐸 ∈ V )
21 17 19 20 syl2anc ⊢ ( 𝜑 → 𝐸 ∈ V )
22 rnexg ⊢ ( 𝐸 ∈ V → ran 𝐸 ∈ V )
23 21 22 syl ⊢ ( 𝜑 → ran 𝐸 ∈ V )
24 3 4 omef ⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
25 6 frnd ⊢ ( 𝜑 → ran 𝐸 ⊆ 𝒫 𝑋 )
26 24 25 fssresd ⊢ ( 𝜑 → ( 𝑂 ↾ ran 𝐸 ) : ran 𝐸 ⟶ ( 0 [,] +∞ ) )
27 23 26 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) ∈ ℝ* )
28 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑂 ∈ OutMeas )
29 28 4 10 omecl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
30 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
31 1 29 30 fmptdf ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑍 ⟶ ( 0 [,] +∞ ) )
32 19 31 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
33 fvex ⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
34 33 rgenw ⊢ ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V
35 dfiun3g ⊢ ( ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
36 34 35 ax-mp ⊢ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) )
37 36 a1i ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
38 6 feqmptd ⊢ ( 𝜑 → 𝐸 = ( 𝑚 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑚 ) ) )
39 nfcv ⊢ Ⅎ 𝑛 𝑚
40 2 39 nffv ⊢ Ⅎ 𝑛 ( 𝐸 ‘ 𝑚 )
41 nfcv ⊢ Ⅎ 𝑚 ( 𝐸 ‘ 𝑛 )
42 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐸 ‘ 𝑚 ) = ( 𝐸 ‘ 𝑛 ) )
43 40 41 42 cbvmpt ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) )
44 43 a1i ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
45 38 44 eqtrd ⊢ ( 𝜑 → 𝐸 = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
46 45 rneqd ⊢ ( 𝜑 → ran 𝐸 = ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
47 46 unieqd ⊢ ( 𝜑 → ∪ ran 𝐸 = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
48 37 47 eqtr4d ⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran 𝐸 )
49 48 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ ran 𝐸 ) )
50 fnrndomg ⊢ ( 𝑍 ∈ V → ( 𝐸 Fn 𝑍 → ran 𝐸 ≼ 𝑍 ) )
51 19 17 50 sylc ⊢ ( 𝜑 → ran 𝐸 ≼ 𝑍 )
52 5 uzct ⊢ 𝑍 ≼ ω
53 52 a1i ⊢ ( 𝜑 → 𝑍 ≼ ω )
54 domtr ⊢ ( ( ran 𝐸 ≼ 𝑍 ∧ 𝑍 ≼ ω ) → ran 𝐸 ≼ ω )
55 51 53 54 syl2anc ⊢ ( 𝜑 → ran 𝐸 ≼ ω )
56 3 4 25 55 omeunile ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ ran 𝐸 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) )
57 49 56 eqbrtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) )
58 ltweuz ⊢ < We ( ℤ≥ ‘ 𝑁 )
59 weeq2 ⊢ ( 𝑍 = ( ℤ≥ ‘ 𝑁 ) → ( < We 𝑍 ↔ < We ( ℤ≥ ‘ 𝑁 ) ) )
60 5 59 ax-mp ⊢ ( < We 𝑍 ↔ < We ( ℤ≥ ‘ 𝑁 ) )
61 58 60 mpbir ⊢ < We 𝑍
62 61 a1i ⊢ ( 𝜑 → < We 𝑍 )
63 19 24 6 62 sge0resrn ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) ≤ ( Σ^ ‘ ( 𝑂 ∘ 𝐸 ) ) )
64 fcompt ⊢ ( ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝐸 : 𝑍 ⟶ 𝒫 𝑋 ) → ( 𝑂 ∘ 𝐸 ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) )
65 nfcv ⊢ Ⅎ 𝑛 𝑂
66 65 40 nffv ⊢ Ⅎ 𝑛 ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) )
67 nfcv ⊢ Ⅎ 𝑚 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) )
68 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
69 66 67 68 cbvmpt ⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
70 69 a1i ⊢ ( ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝐸 : 𝑍 ⟶ 𝒫 𝑋 ) → ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
71 64 70 eqtrd ⊢ ( ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝐸 : 𝑍 ⟶ 𝒫 𝑋 ) → ( 𝑂 ∘ 𝐸 ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
72 24 6 71 syl2anc ⊢ ( 𝜑 → ( 𝑂 ∘ 𝐸 ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
73 72 fveq2d ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ∘ 𝐸 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
74 63 73 breqtrd ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
75 16 27 32 57 74 xrletrd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )