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 ⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t 𝐴 )
Assertion subopnmbl ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ 𝐽 ) → 𝐵 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 subopnmbl.1 ⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t 𝐴 )
2 1 eleq2i ⊢ ( 𝐵 ∈ 𝐽 ↔ 𝐵 ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) )
3 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
4 elrest ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ 𝐴 ∈ dom vol ) → ( 𝐵 ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ ( topGen ‘ ran (,) ) 𝐵 = ( 𝑥 ∩ 𝐴 ) ) )
5 3 4 mpan ⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ∈ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ↔ ∃ 𝑥 ∈ ( topGen ‘ ran (,) ) 𝐵 = ( 𝑥 ∩ 𝐴 ) ) )
6 2 5 bitrid ⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ∈ 𝐽 ↔ ∃ 𝑥 ∈ ( topGen ‘ ran (,) ) 𝐵 = ( 𝑥 ∩ 𝐴 ) ) )
7 opnmbl ⊢ ( 𝑥 ∈ ( topGen ‘ ran (,) ) → 𝑥 ∈ dom vol )
8 id ⊢ ( 𝐴 ∈ dom vol → 𝐴 ∈ dom vol )
9 inmbl ⊢ ( ( 𝑥 ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( 𝑥 ∩ 𝐴 ) ∈ dom vol )
10 7 8 9 syl2anr ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ( topGen ‘ ran (,) ) ) → ( 𝑥 ∩ 𝐴 ) ∈ dom vol )
11 eleq1a ⊢ ( ( 𝑥 ∩ 𝐴 ) ∈ dom vol → ( 𝐵 = ( 𝑥 ∩ 𝐴 ) → 𝐵 ∈ dom vol ) )
12 10 11 syl ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ( topGen ‘ ran (,) ) ) → ( 𝐵 = ( 𝑥 ∩ 𝐴 ) → 𝐵 ∈ dom vol ) )
13 12 rexlimdva ⊢ ( 𝐴 ∈ dom vol → ( ∃ 𝑥 ∈ ( topGen ‘ ran (,) ) 𝐵 = ( 𝑥 ∩ 𝐴 ) → 𝐵 ∈ dom vol ) )
14 6 13 sylbid ⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ∈ 𝐽 → 𝐵 ∈ dom vol ) )
15 14 imp ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ 𝐽 ) → 𝐵 ∈ dom vol )