opnmbl

Description: All open sets are measurable. This proof, via dyadmbl and uniioombl , shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015)

		Ref	Expression
	Assertion	opnmbl	$⊢ A \in topGen (ran (.)) \to A \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ x = z \to \frac{x}{2^{y}} = \frac{z}{2^{y}}$
2		oveq1	$⊢ x = z \to x + 1 = z + 1$
3	2	oveq1d	$⊢ x = z \to \frac{x + 1}{2^{y}} = \frac{z + 1}{2^{y}}$
4	1 3	opeq12d	$⊢ x = z \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ = ⟨\frac{z}{2^{y}}, \frac{z + 1}{2^{y}}⟩$
5		oveq2	$⊢ y = w \to 2^{y} = 2^{w}$
6	5	oveq2d	$⊢ y = w \to \frac{z}{2^{y}} = \frac{z}{2^{w}}$
7	5	oveq2d	$⊢ y = w \to \frac{z + 1}{2^{y}} = \frac{z + 1}{2^{w}}$
8	6 7	opeq12d	$⊢ y = w \to ⟨\frac{z}{2^{y}}, \frac{z + 1}{2^{y}}⟩ = ⟨\frac{z}{2^{w}}, \frac{z + 1}{2^{w}}⟩$
9	4 8	cbvmpov	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) = (z \in ℤ, w \in ℕ_{0} ⟼ ⟨\frac{z}{2^{w}}, \frac{z + 1}{2^{w}}⟩)$
10	9	opnmbllem	$⊢ A \in topGen (ran (.)) \to A \in dom vol$

Metamath Proof Explorer

Theorem opnmbl

Proof