Theorem ovnsupge0

Description: The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnsupge0.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ovnsupge0.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	ovnsupge0.3	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
Assertion	ovnsupge0	⊢ ( 𝜑 → 𝑀 ⊆ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		ovnsupge0.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ovnsupge0.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3		ovnsupge0.3	⊢ 𝑀 = { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) }
4		simp3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) )
5		nnex	⊢ ℕ ∈ V
6	5	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ℕ ∈ V )
7		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
8		nfv	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑗 ∈ ℕ )
9	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑗 ∈ ℕ ) → 𝑋 ∈ Fin )
10		elmapi	⊢ ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → 𝑖 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
11	10	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑗 ∈ ℕ ) → 𝑖 : ℕ ⟶ ( ( ℝ × ℝ ) ↑m 𝑋 ) )
12		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
13	8 9 11 12	ovnprodcl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,) +∞ ) )
14	7 13	sselid	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) ∧ 𝑗 ∈ ℕ ) → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ∈ ( 0 [,] +∞ ) )
15		eqid	⊢ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
16	14 15	fmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
17	6 16	sge0cl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ∈ ( 0 [,] +∞ ) )
18	17	3adant3	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ∈ ( 0 [,] +∞ ) )
19	4 18	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) )
20	19	3adant3l	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∧ ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) )
21	20	3exp	⊢ ( 𝜑 → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) ) ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) → ( 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) → ( ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) ) ) )
23	22	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) → ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) ) )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ* ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) ) )
25		rabss	⊢ ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ( 0 [,] +∞ ) ↔ ∀ 𝑧 ∈ ℝ* ( ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) → 𝑧 ∈ ( 0 [,] +∞ ) ) )
26	24 25	sylibr	⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝐴 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ⊆ ( 0 [,] +∞ ) )
27	3 26	eqsstrid	⊢ ( 𝜑 → 𝑀 ⊆ ( 0 [,] +∞ ) )