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 2 X y j k X . i j k z = sum^ j k X vol . i j k = z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k
12 8 10 11 ovnsupge0 φ y 𝒫 X z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k 0 +∞
13 8 10 11 ovnpnfelsup φ y 𝒫 X +∞ z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k
14 13 ne0d φ y 𝒫 X z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k
15 5 7 12 14 inficc φ y 𝒫 X sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * < 0 +∞
16 3 15 ifcld φ y 𝒫 X if X = 0 sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * < 0 +∞
17 eqid y 𝒫 X if X = 0 sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * < = y 𝒫 X if X = 0 sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * <
18 16 17 fmptd φ y 𝒫 X if X = 0 sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * < : 𝒫 X 0 +∞
19 1 ovnval φ voln* X = y 𝒫 X if X = 0 sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * <
20 19 feq1d φ voln* X : 𝒫 X 0 +∞ y 𝒫 X if X = 0 sup z * | i 2 X y j k X . i j k z = sum^ j k X vol . i j k * < : 𝒫 X 0 +∞
21 18 20 mpbird φ voln* X : 𝒫 X 0 +∞