Metamath Proof Explorer


Theorem ovnome

Description: ( voln*X ) is an outer measure on the space of multidimensional real numbers with dimension equal to the cardinality of the finite set X . Proposition 115D (a) of Fremlin1 p. 30 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnome.1 φ X Fin
Assertion ovnome φ voln* X OutMeas

Proof

Step Hyp Ref Expression
1 ovnome.1 φ X Fin
2 ovexd φ X V
3 1 ovnf φ voln* X : 𝒫 X 0 +∞
4 1 ovn0 φ voln* X = 0
5 1 3ad2ant1 φ x X y x X Fin
6 simp3 φ x X y x y x
7 simp2 φ x X y x x X
8 5 6 7 ovnssle φ x X y x voln* X y voln* X x
9 1 adantr φ a : 𝒫 X X Fin
10 simpr φ a : 𝒫 X a : 𝒫 X
11 9 10 ovnsubadd φ a : 𝒫 X voln* X n a n sum^ n voln* X a n
12 2 3 4 8 11 isomennd φ voln* X OutMeas