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 ffvelrnd φ 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 ffvelrnda φ 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