Metamath Proof Explorer

Theorem opnvonmbl

Description: An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

		Ref	Expression
	Hypotheses	opnvonmbl.x	$⊢ φ \to X \in Fin$
		opnvonmbl.s	$⊢ S = dom voln (X)$
		opnvonmbl.g	$⊢ φ \to G \in TopOpen (X)$
	Assertion	opnvonmbl	$⊢ φ \to G \in S$

Proof

Step	Hyp	Ref	Expression
1		opnvonmbl.x	$⊢ φ \to X \in Fin$
2		opnvonmbl.s	$⊢ S = dom voln (X)$
3		opnvonmbl.g	$⊢ φ \to G \in TopOpen (X)$
4		fveq2	$⊢ k = i \to ([.) \circ f) (k) = ([.) \circ f) (i)$
5	4	cbvixpv	$⊢ \underset{k \in X}{⨉} ([.) \circ f) (k) = \underset{i \in X}{⨉} ([.) \circ f) (i)$
6	5	a1i	$⊢ f = h \to \underset{k \in X}{⨉} ([.) \circ f) (k) = \underset{i \in X}{⨉} ([.) \circ f) (i)$
7		coeq2	$⊢ f = h \to [.) \circ f = [.) \circ h$
8	7	fveq1d	$⊢ f = h \to ([.) \circ f) (i) = ([.) \circ h) (i)$
9	8	ixpeq2dv	$⊢ f = h \to \underset{i \in X}{⨉} ([.) \circ f) (i) = \underset{i \in X}{⨉} ([.) \circ h) (i)$
10	6 9	eqtrd	$⊢ f = h \to \underset{k \in X}{⨉} ([.) \circ f) (k) = \underset{i \in X}{⨉} ([.) \circ h) (i)$
11	10	sseq1d	$⊢ f = h \to (\underset{k \in X}{⨉} ([.) \circ f) (k) \subseteq G \leftrightarrow \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G)$
12	11	cbvrabv	$⊢ \{f \in ({(ℚ \times ℚ)}^{X}) \| \underset{k \in X}{⨉} ([.) \circ f) (k) \subseteq G\} = \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
13	1 2 3 12	opnvonmbllem2	$⊢ φ \to G \in S$