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∈xifi=l−∞yℝ
Assertion hoimbllem ⊢φ→⨉i∈XA⁡iB⁡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∈xifi=l−∞yℝ
7 1 2 4 5 6 hspdifhsp ⊢φ→⨉i∈XA⁡iB⁡i=⋂i∈XiH⁡XB⁡i∖iH⁡XA⁡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→iH⁡XB⁡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→iH⁡XB⁡i∈S
21 4 ffvelcdmda ⊢φ∧i∈X→A⁡i∈ℝ
22 6 13 14 21 hspmbl ⊢φ∧i∈X→iH⁡XA⁡i∈dom⁡voln⁡X
23 22 19 eleqtrd ⊢φ∧i∈X→iH⁡XA⁡i∈S
24 saldifcl2 ⊢S∈SAlg∧iH⁡XB⁡i∈S∧iH⁡XA⁡i∈S→iH⁡XB⁡i∖iH⁡XA⁡i∈S
25 12 20 23 24 syl3anc ⊢φ∧i∈X→iH⁡XB⁡i∖iH⁡XA⁡i∈S
26 9 11 2 25 saliincl ⊢φ→⋂i∈XiH⁡XB⁡i∖iH⁡XA⁡i∈S
27 7 26 eqeltrd ⊢φ→⨉i∈XA⁡iB⁡i∈S