Metamath Proof Explorer

Theorem hoimbl2

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, 8-Apr-2021)

Ref Expression
Hypotheses hoimbl2.k ⊢ Ⅎ 𝑘 𝜑
hoimbl2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoimbl2.s ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
hoimbl2.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
hoimbl2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
Assertion hoimbl2 ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 hoimbl2.k ⊢ Ⅎ 𝑘 𝜑
2 hoimbl2.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 hoimbl2.s ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
4 hoimbl2.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
5 hoimbl2.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → 𝑗 ∈ 𝑋 )
7 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑋
8 1 7 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑋 )
9 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
10 nfcv ⊢ Ⅎ 𝑘 ℝ
11 9 10 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ
12 8 11 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ )
13 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑋 ↔ 𝑗 ∈ 𝑋 ) )
14 13 anbi2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) ) )
15 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
16 15 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) )
17 14 16 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) ) )
18 12 17 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ )
19 nfcv ⊢ Ⅎ 𝑘 𝑗
20 19 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
21 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑋 ↦ 𝐴 )
22 19 20 15 21 fvmptf ⊢ ( ( 𝑗 ∈ 𝑋 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
23 6 18 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
24 19 nfcsb1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
25 24 10 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ
26 8 25 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
27 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
28 27 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
29 14 28 imbi12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) ) )
30 26 29 5 chvarfv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
31 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑘 ∈ 𝑋 ↦ 𝐵 )
32 19 24 27 31 fvmptf ⊢ ( ( 𝑗 ∈ 𝑋 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
33 6 30 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
34 23 33 oveq12d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑋 ) → ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
35 34 ixpeq2dva ⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) = X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
36 nfcv ⊢ Ⅎ 𝑗 ( 𝐴 [,) 𝐵 )
37 nfcv ⊢ Ⅎ 𝑘 [,)
38 9 37 24 nfov ⊢ Ⅎ 𝑘 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
39 15 27 oveq12d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 [,) 𝐵 ) = ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
40 36 38 39 cbvixp ⊢ X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) = X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
41 40 eqcomi ⊢ X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 )
42 41 a1i ⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ⦋ 𝑗 / 𝑘 ⦌ 𝐴 [,) ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) )
43 35 42 eqtr2d ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) = X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) )
44 1 4 21 fmptdf ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℝ )
45 1 5 31 fmptdf ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ℝ )
46 2 3 44 45 hoimbl ⊢ ( 𝜑 → X 𝑗 ∈ 𝑋 ( ( ( 𝑘 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑗 ) [,) ( ( 𝑘 ∈ 𝑋 ↦ 𝐵 ) ‘ 𝑗 ) ) ∈ 𝑆 )
47 43 46 eqeltrd ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( 𝐴 [,) 𝐵 ) ∈ 𝑆 )