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

Proof

Step	Hyp	Ref	Expression
1		orvcgteel.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		orvcgteel.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orvcgteel.3	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
6		brcnvg	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑥 ◡ ≤ 𝐴 ↔ 𝐴 ≤ 𝑥 ) )
7	4 5 6	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ◡ ≤ 𝐴 ↔ 𝐴 ≤ 𝑥 ) )
8	7	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ◡ ≤ 𝐴 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) )
9		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
10	9	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ* )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) → 𝐴 ≤ 𝑥 )
12		ltpnf	⊢ ( 𝑥 ∈ ℝ → 𝑥 < +∞ )
13	12	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) → 𝑥 < +∞ )
14	11 13	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) → ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) )
15	10 14	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) → 𝑥 ∈ ℝ* )
17	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) → 𝐴 ∈ ℝ )
18		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) → 𝐴 ≤ 𝑥 )
19		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) → 𝑥 < +∞ )
20		xrre3	⊢ ( ( ( 𝑥 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) → 𝑥 ∈ ℝ )
21	16 17 18 19 20	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) → 𝑥 ∈ ℝ )
22	21 18	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) )
23	15 22	impbida	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ) ↔ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) )
24	8 23	bitrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ◡ ≤ 𝐴 ) ↔ ( 𝑥 ∈ ℝ* ∧ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) ) )
25	24	rabbidva2	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ◡ ≤ 𝐴 } = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) } )
26	3	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
27		pnfxr	⊢ +∞ ∈ ℝ*
28		icoval	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 [,) +∞ ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) } )
29	26 27 28	sylancl	⊢ ( 𝜑 → ( 𝐴 [,) +∞ ) = { 𝑥 ∈ ℝ* ∣ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < +∞ ) } )
30	25 29	eqtr4d	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ◡ ≤ 𝐴 } = ( 𝐴 [,) +∞ ) )
31		icopnfcld	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
32	3 31	syl	⊢ ( 𝜑 → ( 𝐴 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
33	30 32	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ◡ ≤ 𝐴 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
34	1 2 3 33	orrvccel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ◡ ≤ 𝐴 ) ∈ dom 𝑃 )