Metamath Proof Explorer

Theorem omeiunle

Description: The outer measure of the indexed union of a countable set is less than or equal to the extended sum of the outer measures. The proof uses abrexct rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Vincent Gonzalez, 19-Aug-2026)

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 ffvelcdmda ⊢ φ ∧ 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 eqid ⊢ n ∈ Z ⟼ E ⁡ n = n ∈ Z ⟼ E ⁡ n
51 50 rnmpt ⊢ ran ⁡ n ∈ Z ⟼ E ⁡ n = m | ∃ n ∈ Z m = E ⁡ n
52 46 51 eqtrdi ⊢ φ → ran ⁡ E = m | ∃ n ∈ Z m = E ⁡ n
53 5 uzct ⊢ Z ≼ ω
54 53 a1i ⊢ φ → Z ≼ ω
55 abrexct ⊢ Z ≼ ω → m | ∃ n ∈ Z m = E ⁡ n ≼ ω
56 54 55 syl ⊢ φ → m | ∃ n ∈ Z m = E ⁡ n ≼ ω
57 52 56 eqbrtrd ⊢ φ → ran ⁡ E ≼ ω
58 3 4 25 57 omeunile ⊢ φ → O ⁡ ⋃ ran ⁡ E ≤ sum^ ⁡ O ↾ ran ⁡ E
59 49 58 eqbrtrd ⊢ φ → O ⁡ ⋃ n ∈ Z E ⁡ n ≤ sum^ ⁡ O ↾ ran ⁡ E
60 ltweuz ⊢ < We ℤ ≥ N
61 weeq2 ⊢ Z = ℤ ≥ N → < We Z ↔ < We ℤ ≥ N
62 5 61 ax-mp ⊢ < We Z ↔ < We ℤ ≥ N
63 60 62 mpbir ⊢ < We Z
64 63 a1i ⊢ φ → < We Z
65 19 24 6 64 sge0resrn ⊢ φ → sum^ ⁡ O ↾ ran ⁡ E ≤ sum^ ⁡ O ∘ E
66 fcompt ⊢ O : 𝒫 X ⟶ 0 +∞ ∧ E : Z ⟶ 𝒫 X → O ∘ E = m ∈ Z ⟼ O ⁡ E ⁡ m
67 nfcv ⊢ Ⅎ _ n O
68 67 40 nffv ⊢ Ⅎ _ n O ⁡ E ⁡ m
69 nfcv ⊢ Ⅎ _ m O ⁡ E ⁡ n
70 2fveq3 ⊢ m = n → O ⁡ E ⁡ m = O ⁡ E ⁡ n
71 68 69 70 cbvmpt ⊢ m ∈ Z ⟼ O ⁡ E ⁡ m = n ∈ Z ⟼ O ⁡ E ⁡ n
72 71 a1i ⊢ O : 𝒫 X ⟶ 0 +∞ ∧ E : Z ⟶ 𝒫 X → m ∈ Z ⟼ O ⁡ E ⁡ m = n ∈ Z ⟼ O ⁡ E ⁡ n
73 66 72 eqtrd ⊢ O : 𝒫 X ⟶ 0 +∞ ∧ E : Z ⟶ 𝒫 X → O ∘ E = n ∈ Z ⟼ O ⁡ E ⁡ n
74 24 6 73 syl2anc ⊢ φ → O ∘ E = n ∈ Z ⟼ O ⁡ E ⁡ n
75 74 fveq2d ⊢ φ → sum^ ⁡ O ∘ E = sum^ ⁡ n ∈ Z ⟼ O ⁡ E ⁡ n
76 65 75 breqtrd ⊢ φ → sum^ ⁡ O ↾ ran ⁡ E ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ E ⁡ n
77 16 27 32 59 76 xrletrd ⊢ φ → O ⁡ ⋃ n ∈ Z E ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ E ⁡ n