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 ⊢Ⅎnφ
omeiunlempt.o ⊢φ→O∈OutMeas
omeiunlempt.x ⊢X=⋃dom⁡O
omeiunlempt.z ⊢Z=ℤ≥N
omeiunlempt.e ⊢φ∧n∈Z→E⊆X
Assertion omeiunlempt ⊢φ→O⁡⋃n∈ZE≤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 ⊢Ⅎ_nn∈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∈Zn∈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∈ZE=⋃n∈Zn∈Z⟼E⁡n
22 21 fveq2d ⊢φ→O⁡⋃n∈ZE=O⁡⋃n∈Zn∈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∈ZE≤sum^⁡n∈Z⟼O⁡E↔O⁡⋃n∈Zn∈Z⟼E⁡n≤sum^⁡n∈Z⟼O⁡n∈Z⟼E⁡n
27 16 26 mpbird ⊢φ→O⁡⋃n∈ZE≤sum^⁡n∈Z⟼O⁡E