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

Metamath Proof Explorer

Theorem subopnmbl

Description: Sets which are open in a measurable subspace are measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypothesis subopnmbl.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 A
Assertion subopnmbl ⊢ A ∈ dom ⁡ vol ∧ B ∈ J → B ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 subopnmbl.1 ⊢ J = topGen ⁡ ran ⁡ . ↾ 𝑡 A
2 1 eleq2i ⊢ B ∈ J ↔ B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 A
3 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
4 elrest ⊢ topGen ⁡ ran ⁡ . ∈ Top ∧ A ∈ dom ⁡ vol → B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 A ↔ ∃ x ∈ topGen ⁡ ran ⁡ . B = x ∩ A
5 3 4 mpan ⊢ A ∈ dom ⁡ vol → B ∈ topGen ⁡ ran ⁡ . ↾ 𝑡 A ↔ ∃ x ∈ topGen ⁡ ran ⁡ . B = x ∩ A
6 2 5 bitrid ⊢ A ∈ dom ⁡ vol → B ∈ J ↔ ∃ x ∈ topGen ⁡ ran ⁡ . B = x ∩ A
7 opnmbl ⊢ x ∈ topGen ⁡ ran ⁡ . → x ∈ dom ⁡ vol
8 id ⊢ A ∈ dom ⁡ vol → A ∈ dom ⁡ vol
9 inmbl ⊢ x ∈ dom ⁡ vol ∧ A ∈ dom ⁡ vol → x ∩ A ∈ dom ⁡ vol
10 7 8 9 syl2anr ⊢ A ∈ dom ⁡ vol ∧ x ∈ topGen ⁡ ran ⁡ . → x ∩ A ∈ dom ⁡ vol
11 eleq1a ⊢ x ∩ A ∈ dom ⁡ vol → B = x ∩ A → B ∈ dom ⁡ vol
12 10 11 syl ⊢ A ∈ dom ⁡ vol ∧ x ∈ topGen ⁡ ran ⁡ . → B = x ∩ A → B ∈ dom ⁡ vol
13 12 rexlimdva ⊢ A ∈ dom ⁡ vol → ∃ x ∈ topGen ⁡ ran ⁡ . B = x ∩ A → B ∈ dom ⁡ vol
14 6 13 sylbid ⊢ A ∈ dom ⁡ vol → B ∈ J → B ∈ dom ⁡ vol
15 14 imp ⊢ A ∈ dom ⁡ vol ∧ B ∈ J → B ∈ dom ⁡ vol