Theorem 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 \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to A\in \mathrm{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	$$⊢\left(x\in \mathbb{Z},y\in {\mathbb{N}}_0⟼⟨\frac{x}{2^y},\frac{x+1}{2^y}⟩\right)=\left(z\in \mathbb{Z},w\in {\mathbb{N}}_0⟼⟨\frac{z}{2^w},\frac{z+1}{2^w}⟩\right)$$
10	9	opnmbllem	$$⊢A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to A\in \mathrm{dom}vol$$