Metamath Proof Explorer

Theorem orvcgteel

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

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

Proof

Step Hyp Ref Expression
1 orvcgteel.1 
 |-  ( ph -> P e. Prob )
2 orvcgteel.2 
 |-  ( ph -> X e. ( rRndVar ` P ) )
3 orvcgteel.3 
 |-  ( ph -> A e. RR )
4 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
5 3 adantr 
 |-  ( ( ph /\ x e. RR ) -> A e. RR )
6 brcnvg 
 |-  ( ( x e. RR /\ A e. RR ) -> ( x `' <_ A <-> A <_ x ) )
7 4 5 6 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( x `' <_ A <-> A <_ x ) )
8 7 pm5.32da 
 |-  ( ph -> ( ( x e. RR /\ x `' <_ A ) <-> ( x e. RR /\ A <_ x ) ) )
9 rexr 
 |-  ( x e. RR -> x e. RR* )
10 9 ad2antrl 
 |-  ( ( ph /\ ( x e. RR /\ A <_ x ) ) -> x e. RR* )
11 simprr 
 |-  ( ( ph /\ ( x e. RR /\ A <_ x ) ) -> A <_ x )
12 ltpnf 
 |-  ( x e. RR -> x < +oo )
13 12 ad2antrl 
 |-  ( ( ph /\ ( x e. RR /\ A <_ x ) ) -> x < +oo )
14 11 13 jca 
 |-  ( ( ph /\ ( x e. RR /\ A <_ x ) ) -> ( A <_ x /\ x < +oo ) )
15 10 14 jca 
 |-  ( ( ph /\ ( x e. RR /\ A <_ x ) ) -> ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) )
16 simprl 
 |-  ( ( ph /\ ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) -> x e. RR* )
17 3 adantr 
 |-  ( ( ph /\ ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) -> A e. RR )
18 simprrl 
 |-  ( ( ph /\ ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) -> A <_ x )
19 simprrr 
 |-  ( ( ph /\ ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) -> x < +oo )
20 xrre3 
 |-  ( ( ( x e. RR* /\ A e. RR ) /\ ( A <_ x /\ x < +oo ) ) -> x e. RR )
21 16 17 18 19 20 syl22anc 
 |-  ( ( ph /\ ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) -> x e. RR )
22 21 18 jca 
 |-  ( ( ph /\ ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) -> ( x e. RR /\ A <_ x ) )
23 15 22 impbida 
 |-  ( ph -> ( ( x e. RR /\ A <_ x ) <-> ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) )
24 8 23 bitrd 
 |-  ( ph -> ( ( x e. RR /\ x `' <_ A ) <-> ( x e. RR* /\ ( A <_ x /\ x < +oo ) ) ) )
25 24 rabbidva2 
 |-  ( ph -> { x e. RR | x `' <_ A } = { x e. RR* | ( A <_ x /\ x < +oo ) } )
26 3 rexrd 
 |-  ( ph -> A e. RR* )
27 pnfxr 
 |-  +oo e. RR*
28 icoval 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A [,) +oo ) = { x e. RR* | ( A <_ x /\ x < +oo ) } )
29 26 27 28 sylancl 
 |-  ( ph -> ( A [,) +oo ) = { x e. RR* | ( A <_ x /\ x < +oo ) } )
30 25 29 eqtr4d 
 |-  ( ph -> { x e. RR | x `' <_ A } = ( A [,) +oo ) )
31 icopnfcld 
 |-  ( A e. RR -> ( A [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
32 3 31 syl 
 |-  ( ph -> ( A [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
33 30 32 eqeltrd 
 |-  ( ph -> { x e. RR | x `' <_ A } e. ( Clsd ` ( topGen ` ran (,) ) ) )
34 1 2 3 33 orrvccel 
 |-  ( ph -> ( X oRVC `' <_ A ) e. dom P )