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 φPProb
orvcgteel.2 φXRndVarP
orvcgteel.3 φA
Assertion orvcgteel φX-1RV/cAdomP

Proof

Step Hyp Ref Expression
1 orvcgteel.1 φPProb
2 orvcgteel.2 φXRndVarP
3 orvcgteel.3 φA
4 simpr φxx
5 3 adantr φxA
6 brcnvg xAx-1AAx
7 4 5 6 syl2anc φxx-1AAx
8 7 pm5.32da φxx-1AxAx
9 rexr xx*
10 9 ad2antrl φxAxx*
11 simprr φxAxAx
12 ltpnf xx<+∞
13 12 ad2antrl φxAxx<+∞
14 11 13 jca φxAxAxx<+∞
15 10 14 jca φxAxx*Axx<+∞
16 simprl φx*Axx<+∞x*
17 3 adantr φx*Axx<+∞A
18 simprrl φx*Axx<+∞Ax
19 simprrr φx*Axx<+∞x<+∞
20 xrre3 x*AAxx<+∞x
21 16 17 18 19 20 syl22anc φx*Axx<+∞x
22 21 18 jca φx*Axx<+∞xAx
23 15 22 impbida φxAxx*Axx<+∞
24 8 23 bitrd φxx-1Ax*Axx<+∞
25 24 rabbidva2 φx|x-1A=x*|Axx<+∞
26 3 rexrd φA*
27 pnfxr +∞*
28 icoval A*+∞*A+∞=x*|Axx<+∞
29 26 27 28 sylancl φA+∞=x*|Axx<+∞
30 25 29 eqtr4d φx|x-1A=A+∞
31 icopnfcld AA+∞ClsdtopGenran.
32 3 31 syl φA+∞ClsdtopGenran.
33 30 32 eqeltrd φx|x-1AClsdtopGenran.
34 1 2 3 33 orrvccel φX-1RV/cAdomP