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	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	dstfrv.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	orvclteel.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion	orvclteel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ≤ 𝐴 ) ∈ dom 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dstfrv.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orvclteel.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
5	4	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) ) → 𝑥 ∈ ℝ* )
6		mnflt	⊢ ( 𝑥 ∈ ℝ → -∞ < 𝑥 )
7	6	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) ) → -∞ < 𝑥 )
8		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) ) → 𝑥 ≤ 𝐴 )
9	7 8	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) ) → ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) )
10	5 9	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) ) → ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) )
11		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) → 𝑥 ∈ ℝ* )
12	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
13		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) → -∞ < 𝑥 )
14		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) → 𝑥 ≤ 𝐴 )
15		xrre	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) → 𝑥 ∈ ℝ )
16	11 12 13 14 15	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) → 𝑥 ∈ ℝ )
17	16 14	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) )
18	10 17	impbida	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) ↔ ( 𝑥 ∈ ℝ* ∧ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) ) ) )
19	18	rabbidva2	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } = { 𝑥 ∈ ℝ* ∣ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) } )
20		mnfxr	⊢ -∞ ∈ ℝ*
21	3	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
22		iocval	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ (,] 𝐴 ) = { 𝑥 ∈ ℝ* ∣ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) } )
23	20 21 22	sylancr	⊢ ( 𝜑 → ( -∞ (,] 𝐴 ) = { 𝑥 ∈ ℝ* ∣ ( -∞ < 𝑥 ∧ 𝑥 ≤ 𝐴 ) } )
24	19 23	eqtr4d	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } = ( -∞ (,] 𝐴 ) )
25		iocmnfcld	⊢ ( 𝐴 ∈ ℝ → ( -∞ (,] 𝐴 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
26	3 25	syl	⊢ ( 𝜑 → ( -∞ (,] 𝐴 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
27	24 26	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
28	1 2 3 27	orrvccel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ≤ 𝐴 ) ∈ dom 𝑃 )