This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )