Theorem hoimbl

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	hoimbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	hoimbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
	hoimbl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	hoimbl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
Assertion	hoimbl	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		hoimbl.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		hoimbl.s	⊢ 𝑆 = dom ( voln ‘ 𝑋 )
3		hoimbl.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4		hoimbl.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
6	5	rrnmbl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( ℝ ↑m 𝑋 ) ∈ dom ( voln ‘ 𝑋 ) )
7		reex	⊢ ℝ ∈ V
8		mapdm0	⊢ ( ℝ ∈ V → ( ℝ ↑m ∅ ) = { ∅ } )
9	7 8	ax-mp	⊢ ( ℝ ↑m ∅ ) = { ∅ }
10	9	eqcomi	⊢ { ∅ } = ( ℝ ↑m ∅ )
11	10	a1i	⊢ ( 𝑋 = ∅ → { ∅ } = ( ℝ ↑m ∅ ) )
12		id	⊢ ( 𝑋 = ∅ → 𝑋 = ∅ )
13	12	ixpeq1d	⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = X 𝑖 ∈ ∅ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) )
14		ixp0x	⊢ X 𝑖 ∈ ∅ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = { ∅ }
15	14	a1i	⊢ ( 𝑋 = ∅ → X 𝑖 ∈ ∅ ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = { ∅ } )
16	13 15	eqtrd	⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = { ∅ } )
17		oveq2	⊢ ( 𝑋 = ∅ → ( ℝ ↑m 𝑋 ) = ( ℝ ↑m ∅ ) )
18	11 16 17	3eqtr4d	⊢ ( 𝑋 = ∅ → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ( ℝ ↑m 𝑋 ) )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) = ( ℝ ↑m 𝑋 ) )
20	2	a1i	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → 𝑆 = dom ( voln ‘ 𝑋 ) )
21	19 20	eleq12d	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 ↔ ( ℝ ↑m 𝑋 ) ∈ dom ( voln ‘ 𝑋 ) ) )
22	6 21	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )
23	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ∈ Fin )
24	12	necon3bi	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
25	24	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
26	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐴 : 𝑋 ⟶ ℝ )
27	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → 𝐵 : 𝑋 ⟶ ℝ )
28		id	⊢ ( 𝑤 = 𝑥 → 𝑤 = 𝑥 )
29		eqidd	⊢ ( 𝑤 = 𝑥 → ℝ = ℝ )
30	28	ixpeq1d	⊢ ( 𝑤 = 𝑥 → X 𝑗 ∈ 𝑤 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = X 𝑗 ∈ 𝑥 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) )
31		eqeq1	⊢ ( 𝑗 = 𝑖 → ( 𝑗 = ℎ ↔ 𝑖 = ℎ ) )
32	31	ifbid	⊢ ( 𝑗 = 𝑖 → if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) )
33	32	cbvixpv	⊢ X 𝑗 ∈ 𝑥 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ )
34	33	a1i	⊢ ( 𝑤 = 𝑥 → X 𝑗 ∈ 𝑥 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) )
35	30 34	eqtrd	⊢ ( 𝑤 = 𝑥 → X 𝑗 ∈ 𝑤 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) )
36	28 29 35	mpoeq123dv	⊢ ( 𝑤 = 𝑥 → ( ℎ ∈ 𝑤 , 𝑧 ∈ ℝ ↦ X 𝑗 ∈ 𝑤 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) ) = ( ℎ ∈ 𝑥 , 𝑧 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) ) )
37		eqeq2	⊢ ( ℎ = 𝑙 → ( 𝑖 = ℎ ↔ 𝑖 = 𝑙 ) )
38	37	ifbid	⊢ ( ℎ = 𝑙 → if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑧 ) , ℝ ) )
39	38	ixpeq2dv	⊢ ( ℎ = 𝑙 → X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) = X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑧 ) , ℝ ) )
40		oveq2	⊢ ( 𝑧 = 𝑦 → ( -∞ (,) 𝑧 ) = ( -∞ (,) 𝑦 ) )
41	40	ifeq1d	⊢ ( 𝑧 = 𝑦 → if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑧 ) , ℝ ) = if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
42	41	ixpeq2dv	⊢ ( 𝑧 = 𝑦 → X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑧 ) , ℝ ) = X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
43	39 42	cbvmpov	⊢ ( ℎ ∈ 𝑥 , 𝑧 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) ) = ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) )
44	43	a1i	⊢ ( 𝑤 = 𝑥 → ( ℎ ∈ 𝑥 , 𝑧 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) ) = ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
45	36 44	eqtrd	⊢ ( 𝑤 = 𝑥 → ( ℎ ∈ 𝑤 , 𝑧 ∈ ℝ ↦ X 𝑗 ∈ 𝑤 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) ) = ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
46	45	cbvmptv	⊢ ( 𝑤 ∈ Fin ↦ ( ℎ ∈ 𝑤 , 𝑧 ∈ ℝ ↦ X 𝑗 ∈ 𝑤 if ( 𝑗 = ℎ , ( -∞ (,) 𝑧 ) , ℝ ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑙 ∈ 𝑥 , 𝑦 ∈ ℝ ↦ X 𝑖 ∈ 𝑥 if ( 𝑖 = 𝑙 , ( -∞ (,) 𝑦 ) , ℝ ) ) )
47	23 25 2 26 27 46	hoimbllem	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )
48	22 47	pm2.61dan	⊢ ( 𝜑 → X 𝑖 ∈ 𝑋 ( ( 𝐴 ‘ 𝑖 ) [,) ( 𝐵 ‘ 𝑖 ) ) ∈ 𝑆 )