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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
Assertion	ovnome	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )

Proof

Step	Hyp	Ref	Expression
1		ovnome.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovexd	⊢ ( 𝜑 → ( ℝ ↑m 𝑋 ) ∈ V )
3	1	ovnf	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) : 𝒫 ( ℝ ↑m 𝑋 ) ⟶ ( 0 [,] +∞ ) )
4	1	ovn0	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∅ ) = 0 )
5	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( ℝ ↑m 𝑋 ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑋 ∈ Fin )
6		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( ℝ ↑m 𝑋 ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ⊆ 𝑥 )
7		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( ℝ ↑m 𝑋 ) ∧ 𝑦 ⊆ 𝑥 ) → 𝑥 ⊆ ( ℝ ↑m 𝑋 ) )
8	5 6 7	ovnssle	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ ( ℝ ↑m 𝑋 ) ∧ 𝑦 ⊆ 𝑥 ) → ( ( voln* ‘ 𝑋 ) ‘ 𝑦 ) ≤ ( ( voln* ‘ 𝑋 ) ‘ 𝑥 ) )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) → 𝑋 ∈ Fin )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) → 𝑎 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
11	9 10	ovnsubadd	⊢ ( ( 𝜑 ∧ 𝑎 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝑎 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝑎 ‘ 𝑛 ) ) ) ) )
12	2 3 4 8 11	isomennd	⊢ ( 𝜑 → ( voln* ‘ 𝑋 ) ∈ OutMeas )