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	$⊢ Ⅎ k φ$
	hoimbl2.x	$⊢ φ \to X \in Fin$
	hoimbl2.s	$⊢ S = dom voln (X)$
	hoimbl2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
	hoimbl2.b	$⊢ (φ \land k \in X) \to B \in ℝ$
Assertion	hoimbl2	$⊢ φ \to \underset{k \in X}{⨉} [A, B) \in S$

Proof

Step	Hyp	Ref	Expression
1		hoimbl2.k	$⊢ Ⅎ k φ$
2		hoimbl2.x	$⊢ φ \to X \in Fin$
3		hoimbl2.s	$⊢ S = dom voln (X)$
4		hoimbl2.a	$⊢ (φ \land k \in X) \to A \in ℝ$
5		hoimbl2.b	$⊢ (φ \land k \in X) \to B \in ℝ$
6		simpr	$⊢ (φ \land j \in X) \to j \in X$
7		nfv	$⊢ Ⅎ k j \in X$
8	1 7	nfan	$⊢ Ⅎ k (φ \land j \in X)$
9		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ A$
10		nfcv	$⊢ \underline{Ⅎ} k ℝ$
11	9 10	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ A \in ℝ$
12	8 11	nfim	$⊢ Ⅎ k ((φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ)$
13		eleq1w	$⊢ k = j \to (k \in X \leftrightarrow j \in X)$
14	13	anbi2d	$⊢ k = j \to ((φ \land k \in X) \leftrightarrow (φ \land j \in X))$
15		csbeq1a	$⊢ k = j \to A = ⦋ j / k ⦌ A$
16	15	eleq1d	$⊢ k = j \to (A \in ℝ \leftrightarrow ⦋ j / k ⦌ A \in ℝ)$
17	14 16	imbi12d	$⊢ k = j \to (((φ \land k \in X) \to A \in ℝ) \leftrightarrow ((φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ))$
18	12 17 4	chvarfv	$⊢ (φ \land j \in X) \to ⦋ j / k ⦌ A \in ℝ$
19		nfcv	$⊢ \underline{Ⅎ} k j$
20	19	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ A$
21		eqid	$⊢ (k \in X ⟼ A) = (k \in X ⟼ A)$
22	19 20 15 21	fvmptf	$⊢ (j \in X \land ⦋ j / k ⦌ A \in ℝ) \to (k \in X ⟼ A) (j) = ⦋ j / k ⦌ A$
23	6 18 22	syl2anc	$⊢ (φ \land j \in X) \to (k \in X ⟼ A) (j) = ⦋ j / k ⦌ A$
24	19	nfcsb1	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
25	24 10	nfel	$⊢ Ⅎ k ⦋ j / k ⦌ B \in ℝ$
26	8 25	nfim	$⊢ Ⅎ k ((φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ)$
27		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
28	27	eleq1d	$⊢ k = j \to (B \in ℝ \leftrightarrow ⦋ j / k ⦌ B \in ℝ)$
29	14 28	imbi12d	$⊢ k = j \to (((φ \land k \in X) \to B \in ℝ) \leftrightarrow ((φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ))$
30	26 29 5	chvarfv	$⊢ (φ \land j \in X) \to ⦋ j / k ⦌ B \in ℝ$
31		eqid	$⊢ (k \in X ⟼ B) = (k \in X ⟼ B)$
32	19 24 27 31	fvmptf	$⊢ (j \in X \land ⦋ j / k ⦌ B \in ℝ) \to (k \in X ⟼ B) (j) = ⦋ j / k ⦌ B$
33	6 30 32	syl2anc	$⊢ (φ \land j \in X) \to (k \in X ⟼ B) (j) = ⦋ j / k ⦌ B$
34	23 33	oveq12d	$⊢ (φ \land j \in X) \to [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
35	34	ixpeq2dva	$⊢ φ \to \underset{j \in X}{⨉} [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) = \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
36		nfcv	$⊢ \underline{Ⅎ} j [A, B)$
37		nfcv	$⊢ \underline{Ⅎ} k [.)$
38	9 37 24	nfov	$⊢ \underline{Ⅎ} k [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
39	15 27	oveq12d	$⊢ k = j \to [A, B) = [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
40	36 38 39	cbvixp	$⊢ \underset{k \in X}{⨉} [A, B) = \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B)$
41	40	eqcomi	$⊢ \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = \underset{k \in X}{⨉} [A, B)$
42	41	a1i	$⊢ φ \to \underset{j \in X}{⨉} [⦋ j / k ⦌ A, ⦋ j / k ⦌ B) = \underset{k \in X}{⨉} [A, B)$
43	35 42	eqtr2d	$⊢ φ \to \underset{k \in X}{⨉} [A, B) = \underset{j \in X}{⨉} [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j))$
44	1 4 21	fmptdf	$⊢ φ \to (k \in X ⟼ A) : X ⟶ ℝ$
45	1 5 31	fmptdf	$⊢ φ \to (k \in X ⟼ B) : X ⟶ ℝ$
46	2 3 44 45	hoimbl	$⊢ φ \to \underset{j \in X}{⨉} [(k \in X ⟼ A) (j), (k \in X ⟼ B) (j)) \in S$
47	43 46	eqeltrd	$⊢ φ \to \underset{k \in X}{⨉} [A, B) \in S$

Metamath Proof Explorer

Theorem hoimbl2

Proof