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 ⊢ Ⅎ n φ
omeiunle.ne ⊢ Ⅎ _ n E
omeiunle.o ⊢ φ → O ∈ OutMeas
omeiunle.x ⊢ X = ⋃ dom ⁡ O
omeiunle.z ⊢ Z = ℤ ≥ N
omeiunle.e ⊢ φ → E : Z ⟶ 𝒫 X
Assertion omeiunle ⊢ φ → O ⁡ ⋃ n ∈ Z E ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ E ⁡ n

Proof

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