Metamath Proof Explorer

Theorem ovnf

Description: The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnf.1 ⊢φ→X∈Fin
Assertion ovnf ⊢φ→voln*⁡X:𝒫ℝX⟶0+∞

Proof

Step Hyp Ref Expression
1 ovnf.1 ⊢φ→X∈Fin
2 0e0iccpnf ⊢0∈0+∞
3 2 a1i ⊢φ∧y∈𝒫ℝX→0∈0+∞
4 0xr ⊢0∈ℝ*
5 4 a1i ⊢φ∧y∈𝒫ℝX→0∈ℝ*
6 pnfxr ⊢+∞∈ℝ*
7 6 a1i ⊢φ∧y∈𝒫ℝX→+∞∈ℝ*
8 1 adantr ⊢φ∧y∈𝒫ℝX→X∈Fin
9 elpwi ⊢y∈𝒫ℝX→y⊆ℝX
10 9 adantl ⊢φ∧y∈𝒫ℝX→y⊆ℝX
11 eqid ⊢z∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡k=z∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡k
12 8 10 11 ovnsupge0 ⊢φ∧y∈𝒫ℝX→z∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡k⊆0+∞
13 8 10 11 ovnpnfelsup ⊢φ∧y∈𝒫ℝX→+∞∈z∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡k
14 13 ne0d ⊢φ∧y∈𝒫ℝX→z∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡k≠∅
15 5 7 12 14 inficc ⊢φ∧y∈𝒫ℝX→supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<∈0+∞
16 3 15 ifcld ⊢φ∧y∈𝒫ℝX→ifX=∅0supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<∈0+∞
17 eqid ⊢y∈𝒫ℝX⟼ifX=∅0supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<=y∈𝒫ℝX⟼ifX=∅0supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<
18 16 17 fmptd ⊢φ→y∈𝒫ℝX⟼ifX=∅0supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<:𝒫ℝX⟶0+∞
19 1 ovnval ⊢φ→voln*⁡X=y∈𝒫ℝX⟼ifX=∅0supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<
20 19 feq1d ⊢φ→voln*⁡X:𝒫ℝX⟶0+∞↔y∈𝒫ℝX⟼ifX=∅0supz∈ℝ*|∃i∈ℝ2Xℕy⊆⋃j∈ℕ⨉k∈X.∘i⁡j⁡k∧z=sum^⁡j∈ℕ⟼∏k∈Xvol⁡.∘i⁡j⁡kℝ*<:𝒫ℝX⟶0+∞
21 18 20 mpbird ⊢φ→voln*⁡X:𝒫ℝX⟶0+∞