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 ⊢ φ → P ∈ Prob
dstfrv.2 ⊢ φ → X ∈ RndVar ℝ ⁡ P
orvclteel.1 ⊢ φ → A ∈ ℝ
Assertion orvclteel ⊢ φ → X ≤ RV/c A ∈ dom ⁡ P

Proof

Step Hyp Ref Expression
1 dstfrv.1 ⊢ φ → P ∈ Prob
2 dstfrv.2 ⊢ φ → X ∈ RndVar ℝ ⁡ P
3 orvclteel.1 ⊢ φ → A ∈ ℝ
4 rexr ⊢ x ∈ ℝ → x ∈ ℝ *
5 4 ad2antrl ⊢ φ ∧ x ∈ ℝ ∧ x ≤ A → x ∈ ℝ *
6 mnflt ⊢ x ∈ ℝ → −∞ < x
7 6 ad2antrl ⊢ φ ∧ x ∈ ℝ ∧ x ≤ A → −∞ < x
8 simprr ⊢ φ ∧ x ∈ ℝ ∧ x ≤ A → x ≤ A
9 7 8 jca ⊢ φ ∧ x ∈ ℝ ∧ x ≤ A → −∞ < x ∧ x ≤ A
10 5 9 jca ⊢ φ ∧ x ∈ ℝ ∧ x ≤ A → x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A
11 simprl ⊢ φ ∧ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A → x ∈ ℝ *
12 3 adantr ⊢ φ ∧ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A → A ∈ ℝ
13 simprrl ⊢ φ ∧ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A → −∞ < x
14 simprrr ⊢ φ ∧ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A → x ≤ A
15 xrre ⊢ x ∈ ℝ * ∧ A ∈ ℝ ∧ −∞ < x ∧ x ≤ A → x ∈ ℝ
16 11 12 13 14 15 syl22anc ⊢ φ ∧ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A → x ∈ ℝ
17 16 14 jca ⊢ φ ∧ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A → x ∈ ℝ ∧ x ≤ A
18 10 17 impbida ⊢ φ → x ∈ ℝ ∧ x ≤ A ↔ x ∈ ℝ * ∧ −∞ < x ∧ x ≤ A
19 18 rabbidva2 ⊢ φ → x ∈ ℝ | x ≤ A = x ∈ ℝ * | −∞ < x ∧ x ≤ A
20 mnfxr ⊢ −∞ ∈ ℝ *
21 3 rexrd ⊢ φ → A ∈ ℝ *
22 iocval ⊢ −∞ ∈ ℝ * ∧ A ∈ ℝ * → −∞ A = x ∈ ℝ * | −∞ < x ∧ x ≤ A
23 20 21 22 sylancr ⊢ φ → −∞ A = x ∈ ℝ * | −∞ < x ∧ x ≤ A
24 19 23 eqtr4d ⊢ φ → x ∈ ℝ | x ≤ A = −∞ A
25 iocmnfcld ⊢ A ∈ ℝ → −∞ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
26 3 25 syl ⊢ φ → −∞ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
27 24 26 eqeltrd ⊢ φ → x ∈ ℝ | x ≤ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
28 1 2 3 27 orrvccel ⊢ φ → X ≤ RV/c A ∈ dom ⁡ P