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