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	$$⊢\phi \to X\in \mathrm{Fin}$$
	hoimbl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
	hoimbl.a	$$⊢\phi \to A:X⟶ℝ$$
	hoimbl.b	$$⊢\phi \to B:X⟶ℝ$$
Assertion	hoimbl	$$⊢\phi \to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		hoimbl.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		hoimbl.s	$$⊢S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
3		hoimbl.a	$$⊢\phi \to A:X⟶ℝ$$
4		hoimbl.b	$$⊢\phi \to B:X⟶ℝ$$
5	1	adantr	$$⊢\left(\phi \wedge X=\varnothing \right)\to X\in \mathrm{Fin}$$
6	5	rrnmbl	$$⊢\left(\phi \wedge X=\varnothing \right)\to {ℝ}^X\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
7		reex	$$⊢ℝ\in \mathrm{V}$$
8		mapdm0	$$⊢ℝ\in \mathrm{V}\to {ℝ}^{\varnothing }=\left\{\varnothing \right\}$$
9	7 8	ax-mp	$$⊢{ℝ}^{\varnothing }=\left\{\varnothing \right\}$$
10	9	eqcomi	$$⊢\left\{\varnothing \right\}={ℝ}^{\varnothing }$$
11	10	a1i	$$⊢X=\varnothing \to \left\{\varnothing \right\}={ℝ}^{\varnothing }$$
12		id	$$⊢X=\varnothing \to X=\varnothing$$
13	12	ixpeq1d	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)=\underset{i\in \varnothing }{⨉}\left[A\left(i\right),B\left(i\right)\right)$$
14		ixp0x	$$⊢\underset{i\in \varnothing }{⨉}\left[A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
15	14	a1i	$$⊢X=\varnothing \to \underset{i\in \varnothing }{⨉}\left[A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
16	13 15	eqtrd	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)=\left\{\varnothing \right\}$$
17		oveq2	$$⊢X=\varnothing \to {ℝ}^X={ℝ}^{\varnothing }$$
18	11 16 17	3eqtr4d	$$⊢X=\varnothing \to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)={ℝ}^X$$
19	18	adantl	$$⊢\left(\phi \wedge X=\varnothing \right)\to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)={ℝ}^X$$
20	2	a1i	$$⊢\left(\phi \wedge X=\varnothing \right)\to S=\mathrm{dom}\mathrm{voln}\left(X\right)$$
21	19 20	eleq12d	$$⊢\left(\phi \wedge X=\varnothing \right)\to \left(\underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)\in S\leftrightarrow {ℝ}^X\in \mathrm{dom}\mathrm{voln}\left(X\right)\right)$$
22	6 21	mpbird	$$⊢\left(\phi \wedge X=\varnothing \right)\to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)\in S$$
23	1	adantr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to X\in \mathrm{Fin}$$
24	12	necon3bi	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
25	24	adantl	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to X\ne \varnothing$$
26	3	adantr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to A:X⟶ℝ$$
27	4	adantr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to B:X⟶ℝ$$
28		id	$$⊢w=x\to w=x$$
29		eqidd	$$⊢w=x\to ℝ=ℝ$$
30	28	ixpeq1d	$$⊢w=x\to \underset{j\in w}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)=\underset{j\in x}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)$$
31		eqeq1	$$⊢j=i\to \left(j=h\leftrightarrow i=h\right)$$
32	31	ifbid	$$⊢j=i\to if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)=if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)$$
33	32	cbvixpv	$$⊢\underset{j\in x}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)=\underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)$$
34	33	a1i	$$⊢w=x\to \underset{j\in x}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)=\underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)$$
35	30 34	eqtrd	$$⊢w=x\to \underset{j\in w}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)=\underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)$$
36	28 29 35	mpoeq123dv	$$⊢w=x\to \left(h\in w,z\in ℝ⟼\underset{j\in w}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)\right)=\left(h\in x,z\in ℝ⟼\underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)\right)$$
37		eqeq2	$$⊢h=l\to \left(i=h\leftrightarrow i=l\right)$$
38	37	ifbid	$$⊢h=l\to if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)=if\left(i=l,\left(\mathrm{-\infty },z\right),ℝ\right)$$
39	38	ixpeq2dv	$$⊢h=l\to \underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)=\underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },z\right),ℝ\right)$$
40		oveq2	$$⊢z=y\to \left(\mathrm{-\infty },z\right)=\left(\mathrm{-\infty },y\right)$$
41	40	ifeq1d	$$⊢z=y\to if\left(i=l,\left(\mathrm{-\infty },z\right),ℝ\right)=if\left(i=l,\left(\mathrm{-\infty },y\right),ℝ\right)$$
42	41	ixpeq2dv	$$⊢z=y\to \underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },z\right),ℝ\right)=\underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },y\right),ℝ\right)$$
43	39 42	cbvmpov	$$⊢\left(h\in x,z\in ℝ⟼\underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)\right)=\left(l\in x,y\in ℝ⟼\underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },y\right),ℝ\right)\right)$$
44	43	a1i	$$⊢w=x\to \left(h\in x,z\in ℝ⟼\underset{i\in x}{⨉}if\left(i=h,\left(\mathrm{-\infty },z\right),ℝ\right)\right)=\left(l\in x,y\in ℝ⟼\underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },y\right),ℝ\right)\right)$$
45	36 44	eqtrd	$$⊢w=x\to \left(h\in w,z\in ℝ⟼\underset{j\in w}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)\right)=\left(l\in x,y\in ℝ⟼\underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },y\right),ℝ\right)\right)$$
46	45	cbvmptv	$$⊢\left(w\in \mathrm{Fin}⟼\left(h\in w,z\in ℝ⟼\underset{j\in w}{⨉}if\left(j=h,\left(\mathrm{-\infty },z\right),ℝ\right)\right)\right)=\left(x\in \mathrm{Fin}⟼\left(l\in x,y\in ℝ⟼\underset{i\in x}{⨉}if\left(i=l,\left(\mathrm{-\infty },y\right),ℝ\right)\right)\right)$$
47	23 25 2 26 27 46	hoimbllem	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)\in S$$
48	22 47	pm2.61dan	$$⊢\phi \to \underset{i\in X}{⨉}\left[A\left(i\right),B\left(i\right)\right)\in S$$