Metamath Proof Explorer

Theorem hoimbllem

Description: Any n-dimensional half-open interval is Lebesgue measurable. This is a substep of Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoimbllem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoimbllem.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
hoimbllem.s ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
hoimbllem.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
hoimbllem.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
hoimbllem.h ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
Assertion hoimbllem ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 hoimbllem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 hoimbllem.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 hoimbllem.s ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
4 hoimbllem.a ⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
5 hoimbllem.b ⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
6 hoimbllem.h ⊢ 𝐻 = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
7 1 2 4 5 6 hspdifhsp ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) )
8 1 vonmea ⊢ ( 𝜑 → ( voln ‘ 𝑋 ) ∈ Meas )
9 8 3 dmmeasal ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
10 fict ⊢ ( 𝑋 ∈ Fin → 𝑋 ≼ ω )
11 1 10 syl ⊢ ( 𝜑 → 𝑋 ≼ ω )
12 9 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑆 ∈ SAlg )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑋 ∈ Fin )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → 𝐵 : 𝑋 ⟶ ℝ )
16 15 14 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
17 6 13 14 16 hspmbl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∈ dom ( voln ‘ 𝑋 ) )
18 3 eqcomi ⊢ dom ( voln ‘ 𝑋 ) = 𝑆
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → dom ( voln ‘ 𝑋 ) = 𝑆 )
20 17 19 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )
21 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
22 6 13 14 21 hspmbl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ∈ dom ( voln ‘ 𝑋 ) )
23 22 19 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ∈ 𝑆 )
24 saldifcl2 ⊢ ( ( 𝑆 ∈ SAlg ∧ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 ∧ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ∈ 𝑆 ) → ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∈ 𝑆 )
25 12 20 23 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∈ 𝑆 )
26 9 11 2 25 saliincl ⊢ ( 𝜑 → ∩ 𝑖 ∈ 𝑋 ( ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐵 ‘ 𝑖 ) ) ∖ ( 𝑖 ( 𝐻 ‘ 𝑋 ) ( 𝐴 ‘ 𝑖 ) ) ) ∈ 𝑆 )
27 7 26 eqeltrd ⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )