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 ⊢ φ → X ∈ Fin
hoimbllem.n ⊢ φ → X ≠ ∅
hoimbllem.s ⊢ S = dom ⁡ voln ⁡ X
hoimbllem.a ⊢ φ → A : X ⟶ ℝ
hoimbllem.b ⊢ φ → B : X ⟶ ℝ
hoimbllem.h ⊢ H = x ∈ Fin ⟼ l ∈ x , y ∈ ℝ ⟼ ⨉ i ∈ x if i = l −∞ y ℝ
Assertion hoimbllem ⊢ φ → ⨉ i ∈ X A ⁡ i B ⁡ i ∈ S

Proof

Step Hyp Ref Expression
1 hoimbllem.x ⊢ φ → X ∈ Fin
2 hoimbllem.n ⊢ φ → X ≠ ∅
3 hoimbllem.s ⊢ S = dom ⁡ voln ⁡ X
4 hoimbllem.a ⊢ φ → A : X ⟶ ℝ
5 hoimbllem.b ⊢ φ → B : X ⟶ ℝ
6 hoimbllem.h ⊢ H = x ∈ Fin ⟼ l ∈ x , y ∈ ℝ ⟼ ⨉ i ∈ x if i = l −∞ y ℝ
7 1 2 4 5 6 hspdifhsp ⊢ φ → ⨉ i ∈ X A ⁡ i B ⁡ i = ⋂ i ∈ X i H ⁡ X B ⁡ i ∖ i H ⁡ X A ⁡ i
8 1 vonmea ⊢ φ → voln ⁡ X ∈ Meas
9 8 3 dmmeasal ⊢ φ → S ∈ SAlg
10 fict ⊢ X ∈ Fin → X ≼ ω
11 1 10 syl ⊢ φ → X ≼ ω
12 9 adantr ⊢ φ ∧ i ∈ X → S ∈ SAlg
13 1 adantr ⊢ φ ∧ i ∈ X → X ∈ Fin
14 simpr ⊢ φ ∧ i ∈ X → i ∈ X
15 5 adantr ⊢ φ ∧ i ∈ X → B : X ⟶ ℝ
16 15 14 ffvelcdmd ⊢ φ ∧ i ∈ X → B ⁡ i ∈ ℝ
17 6 13 14 16 hspmbl ⊢ φ ∧ i ∈ X → i H ⁡ X B ⁡ i ∈ dom ⁡ voln ⁡ X
18 3 eqcomi ⊢ dom ⁡ voln ⁡ X = S
19 18 a1i ⊢ φ ∧ i ∈ X → dom ⁡ voln ⁡ X = S
20 17 19 eleqtrd ⊢ φ ∧ i ∈ X → i H ⁡ X B ⁡ i ∈ S
21 4 ffvelcdmda ⊢ φ ∧ i ∈ X → A ⁡ i ∈ ℝ
22 6 13 14 21 hspmbl ⊢ φ ∧ i ∈ X → i H ⁡ X A ⁡ i ∈ dom ⁡ voln ⁡ X
23 22 19 eleqtrd ⊢ φ ∧ i ∈ X → i H ⁡ X A ⁡ i ∈ S
24 saldifcl2 ⊢ S ∈ SAlg ∧ i H ⁡ X B ⁡ i ∈ S ∧ i H ⁡ X A ⁡ i ∈ S → i H ⁡ X B ⁡ i ∖ i H ⁡ X A ⁡ i ∈ S
25 12 20 23 24 syl3anc ⊢ φ ∧ i ∈ X → i H ⁡ X B ⁡ i ∖ i H ⁡ X A ⁡ i ∈ S
26 9 11 2 25 saliincl ⊢ φ → ⋂ i ∈ X i H ⁡ X B ⁡ i ∖ i H ⁡ X A ⁡ i ∈ S
27 7 26 eqeltrd ⊢ φ → ⨉ i ∈ X A ⁡ i B ⁡ i ∈ S