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	syl5bb	⊢ ( 𝐴 ∈ 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 )