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 (,) ) |`t A )
Assertion subopnmbl 
|- ( ( A e. dom vol /\ B e. J ) -> B e. dom vol )

Proof

Step Hyp Ref Expression
1 subopnmbl.1 
 |-  J = ( ( topGen ` ran (,) ) |`t A )
2 1 eleq2i 
 |-  ( B e. J <-> B e. ( ( topGen ` ran (,) ) |`t A ) )
3 retop 
 |-  ( topGen ` ran (,) ) e. Top
4 elrest 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ A e. dom vol ) -> ( B e. ( ( topGen ` ran (,) ) |`t A ) <-> E. x e. ( topGen ` ran (,) ) B = ( x i^i A ) ) )
5 3 4 mpan 
 |-  ( A e. dom vol -> ( B e. ( ( topGen ` ran (,) ) |`t A ) <-> E. x e. ( topGen ` ran (,) ) B = ( x i^i A ) ) )
6 2 5 syl5bb 
 |-  ( A e. dom vol -> ( B e. J <-> E. x e. ( topGen ` ran (,) ) B = ( x i^i A ) ) )
7 opnmbl 
 |-  ( x e. ( topGen ` ran (,) ) -> x e. dom vol )
8 id 
 |-  ( A e. dom vol -> A e. dom vol )
9 inmbl 
 |-  ( ( x e. dom vol /\ A e. dom vol ) -> ( x i^i A ) e. dom vol )
10 7 8 9 syl2anr 
 |-  ( ( A e. dom vol /\ x e. ( topGen ` ran (,) ) ) -> ( x i^i A ) e. dom vol )
11 eleq1a 
 |-  ( ( x i^i A ) e. dom vol -> ( B = ( x i^i A ) -> B e. dom vol ) )
12 10 11 syl 
 |-  ( ( A e. dom vol /\ x e. ( topGen ` ran (,) ) ) -> ( B = ( x i^i A ) -> B e. dom vol ) )
13 12 rexlimdva 
 |-  ( A e. dom vol -> ( E. x e. ( topGen ` ran (,) ) B = ( x i^i A ) -> B e. dom vol ) )
14 6 13 sylbid 
 |-  ( A e. dom vol -> ( B e. J -> B e. dom vol ) )
15 14 imp 
 |-  ( ( A e. dom vol /\ B e. J ) -> B e. dom vol )