Metamath Proof Explorer

Theorem orvclteel

Description: Preimage maps produced by the "less than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017)

Ref Expression
Hypotheses dstfrv.1 
|- ( ph -> P e. Prob )
dstfrv.2 
|- ( ph -> X e. ( rRndVar ` P ) )
orvclteel.1 
|- ( ph -> A e. RR )
Assertion orvclteel 
|- ( ph -> ( X oRVC <_ A ) e. dom P )

Proof

Step Hyp Ref Expression
1 dstfrv.1 
 |-  ( ph -> P e. Prob )
2 dstfrv.2 
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 orvclteel.1 
 |-  ( ph -> A e. RR )
4 rexr 
 |-  ( x e. RR -> x e. RR* )
5 4 ad2antrl 
 |-  ( ( ph /\ ( x e. RR /\ x <_ A ) ) -> x e. RR* )
6 mnflt 
 |-  ( x e. RR -> -oo < x )
7 6 ad2antrl 
 |-  ( ( ph /\ ( x e. RR /\ x <_ A ) ) -> -oo < x )
8 simprr 
 |-  ( ( ph /\ ( x e. RR /\ x <_ A ) ) -> x <_ A )
9 7 8 jca 
 |-  ( ( ph /\ ( x e. RR /\ x <_ A ) ) -> ( -oo < x /\ x <_ A ) )
10 5 9 jca 
 |-  ( ( ph /\ ( x e. RR /\ x <_ A ) ) -> ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) )
11 simprl 
 |-  ( ( ph /\ ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) -> x e. RR* )
12 3 adantr 
 |-  ( ( ph /\ ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) -> A e. RR )
13 simprrl 
 |-  ( ( ph /\ ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) -> -oo < x )
14 simprrr 
 |-  ( ( ph /\ ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) -> x <_ A )
15 xrre 
 |-  ( ( ( x e. RR* /\ A e. RR ) /\ ( -oo < x /\ x <_ A ) ) -> x e. RR )
16 11 12 13 14 15 syl22anc 
 |-  ( ( ph /\ ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) -> x e. RR )
17 16 14 jca 
 |-  ( ( ph /\ ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) -> ( x e. RR /\ x <_ A ) )
18 10 17 impbida 
 |-  ( ph -> ( ( x e. RR /\ x <_ A ) <-> ( x e. RR* /\ ( -oo < x /\ x <_ A ) ) ) )
19 18 rabbidva2 
 |-  ( ph -> { x e. RR | x <_ A } = { x e. RR* | ( -oo < x /\ x <_ A ) } )
20 mnfxr 
 |-  -oo e. RR*
21 3 rexrd 
 |-  ( ph -> A e. RR* )
22 iocval 
 |-  ( ( -oo e. RR* /\ A e. RR* ) -> ( -oo (,] A ) = { x e. RR* | ( -oo < x /\ x <_ A ) } )
23 20 21 22 sylancr 
 |-  ( ph -> ( -oo (,] A ) = { x e. RR* | ( -oo < x /\ x <_ A ) } )
24 19 23 eqtr4d 
 |-  ( ph -> { x e. RR | x <_ A } = ( -oo (,] A ) )
25 iocmnfcld 
 |-  ( A e. RR -> ( -oo (,] A ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
26 3 25 syl 
 |-  ( ph -> ( -oo (,] A ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
27 24 26 eqeltrd 
 |-  ( ph -> { x e. RR | x <_ A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
28 1 2 3 27 orrvccel 
 |-  ( ph -> ( X oRVC <_ A ) e. dom P )