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	⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 / ( 2 ↑ 𝑦 ) ) = ( 𝑧 / ( 2 ↑ 𝑦 ) ) )
2		oveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 + 1 ) = ( 𝑧 + 1 ) )
3	2	oveq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) = ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑦 ) ) )
4	1 3	opeq12d	⊢ ( 𝑥 = 𝑧 → ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ = ⟨ ( 𝑧 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
5		oveq2	⊢ ( 𝑦 = 𝑤 → ( 2 ↑ 𝑦 ) = ( 2 ↑ 𝑤 ) )
6	5	oveq2d	⊢ ( 𝑦 = 𝑤 → ( 𝑧 / ( 2 ↑ 𝑦 ) ) = ( 𝑧 / ( 2 ↑ 𝑤 ) ) )
7	5	oveq2d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑦 ) ) = ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑤 ) ) )
8	6 7	opeq12d	⊢ ( 𝑦 = 𝑤 → ⟨ ( 𝑧 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ = ⟨ ( 𝑧 / ( 2 ↑ 𝑤 ) ) , ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑤 ) ) ⟩ )
9	4 8	cbvmpov	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) = ( 𝑧 ∈ ℤ , 𝑤 ∈ ℕ0 ↦ ⟨ ( 𝑧 / ( 2 ↑ 𝑤 ) ) , ( ( 𝑧 + 1 ) / ( 2 ↑ 𝑤 ) ) ⟩ )
10	9	opnmbllem	⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )