Metamath Proof Explorer

Theorem omeiunlempt

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. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omeiunlempt.nph ⊢ Ⅎ n φ
omeiunlempt.o ⊢ φ → O ∈ OutMeas
omeiunlempt.x ⊢ X = ⋃ dom ⁡ O
omeiunlempt.z ⊢ Z = ℤ ≥ N
omeiunlempt.e ⊢ φ ∧ n ∈ Z → E ⊆ X
Assertion omeiunlempt ⊢ φ → O ⁡ ⋃ n ∈ Z E ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ E

Proof

Step Hyp Ref Expression
1 omeiunlempt.nph ⊢ Ⅎ n φ
2 omeiunlempt.o ⊢ φ → O ∈ OutMeas
3 omeiunlempt.x ⊢ X = ⋃ dom ⁡ O
4 omeiunlempt.z ⊢ Z = ℤ ≥ N
5 omeiunlempt.e ⊢ φ ∧ n ∈ Z → E ⊆ X
6 nfmpt1 ⊢ Ⅎ _ n n ∈ Z ⟼ E
7 2 3 unidmex ⊢ φ → X ∈ V
8 7 adantr ⊢ φ ∧ n ∈ Z → X ∈ V
9 ssexg ⊢ E ⊆ X ∧ X ∈ V → E ∈ V
10 5 8 9 syl2anc ⊢ φ ∧ n ∈ Z → E ∈ V
11 elpwg ⊢ E ∈ V → E ∈ 𝒫 X ↔ E ⊆ X
12 10 11 syl ⊢ φ ∧ n ∈ Z → E ∈ 𝒫 X ↔ E ⊆ X
13 5 12 mpbird ⊢ φ ∧ n ∈ Z → E ∈ 𝒫 X
14 eqid ⊢ n ∈ Z ⟼ E = n ∈ Z ⟼ E
15 1 13 14 fmptdf ⊢ φ → n ∈ Z ⟼ E : Z ⟶ 𝒫 X
16 1 6 2 3 4 15 omeiunle ⊢ φ → O ⁡ ⋃ n ∈ Z n ∈ Z ⟼ E ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ n ∈ Z ⟼ E ⁡ n
17 simpr ⊢ φ ∧ n ∈ Z → n ∈ Z
18 14 fvmpt2 ⊢ n ∈ Z ∧ E ∈ V → n ∈ Z ⟼ E ⁡ n = E
19 17 10 18 syl2anc ⊢ φ ∧ n ∈ Z → n ∈ Z ⟼ E ⁡ n = E
20 19 eqcomd ⊢ φ ∧ n ∈ Z → E = n ∈ Z ⟼ E ⁡ n
21 1 20 iuneq2df ⊢ φ → ⋃ n ∈ Z E = ⋃ n ∈ Z n ∈ Z ⟼ E ⁡ n
22 21 fveq2d ⊢ φ → O ⁡ ⋃ n ∈ Z E = O ⁡ ⋃ n ∈ Z n ∈ Z ⟼ E ⁡ n
23 20 fveq2d ⊢ φ ∧ n ∈ Z → O ⁡ E = O ⁡ n ∈ Z ⟼ E ⁡ n
24 1 23 mpteq2da ⊢ φ → n ∈ Z ⟼ O ⁡ E = n ∈ Z ⟼ O ⁡ n ∈ Z ⟼ E ⁡ n
25 24 fveq2d ⊢ φ → sum^ ⁡ n ∈ Z ⟼ O ⁡ E = sum^ ⁡ n ∈ Z ⟼ O ⁡ n ∈ Z ⟼ E ⁡ n
26 22 25 breq12d ⊢ φ → O ⁡ ⋃ n ∈ Z E ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ E ↔ O ⁡ ⋃ n ∈ Z n ∈ Z ⟼ E ⁡ n ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ n ∈ Z ⟼ E ⁡ n
27 16 26 mpbird ⊢ φ → O ⁡ ⋃ n ∈ Z E ≤ sum^ ⁡ n ∈ Z ⟼ O ⁡ E