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	$$⊢\phi \to P\in \mathrm{Prob}$$
	dstfrv.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
	orvclteel.1	$$⊢\phi \to A\in ℝ$$
Assertion	orvclteel	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}A\in \mathrm{dom}P$$

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		dstfrv.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
3		orvclteel.1	$$⊢\phi \to A\in ℝ$$
4		rexr	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
5	4	ad2antrl	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge x\le A\right)\right)\to x\in {ℝ}^{*}$$
6		mnflt	$$⊢x\in ℝ\to \mathrm{-\infty }<x$$
7	6	ad2antrl	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge x\le A\right)\right)\to \mathrm{-\infty }<x$$
8		simprr	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge x\le A\right)\right)\to x\le A$$
9	7 8	jca	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge x\le A\right)\right)\to \left(\mathrm{-\infty }<x\wedge x\le A\right)$$
10	5 9	jca	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge x\le A\right)\right)\to \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)$$
11		simprl	$$⊢\left(\phi \wedge \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)\to x\in {ℝ}^{*}$$
12	3	adantr	$$⊢\left(\phi \wedge \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)\to A\in ℝ$$
13		simprrl	$$⊢\left(\phi \wedge \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)\to \mathrm{-\infty }<x$$
14		simprrr	$$⊢\left(\phi \wedge \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)\to x\le A$$
15		xrre	$$⊢\left(\left(x\in {ℝ}^{*}\wedge A\in ℝ\right)\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\to x\in ℝ$$
16	11 12 13 14 15	syl22anc	$$⊢\left(\phi \wedge \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)\to x\in ℝ$$
17	16 14	jca	$$⊢\left(\phi \wedge \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)\to \left(x\in ℝ\wedge x\le A\right)$$
18	10 17	impbida	$$⊢\phi \to \left(\left(x\in ℝ\wedge x\le A\right)\leftrightarrow \left(x\in {ℝ}^{*}\wedge \left(\mathrm{-\infty }<x\wedge x\le A\right)\right)\right)$$
19	18	rabbidva2	$$⊢\phi \to \left\{x\in ℝ|x\le A\right\}=\left\{x\in {ℝ}^{*}|\left(\mathrm{-\infty }<x\wedge x\le A\right)\right\}$$
20		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
21	3	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
22		iocval	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty },A\right]=\left\{x\in {ℝ}^{*}|\left(\mathrm{-\infty }<x\wedge x\le A\right)\right\}$$
23	20 21 22	sylancr	$$⊢\phi \to \left(\mathrm{-\infty },A\right]=\left\{x\in {ℝ}^{*}|\left(\mathrm{-\infty }<x\wedge x\le A\right)\right\}$$
24	19 23	eqtr4d	$$⊢\phi \to \left\{x\in ℝ|x\le A\right\}=\left(\mathrm{-\infty },A\right]$$
25		iocmnfcld	$$⊢A\in ℝ\to \left(\mathrm{-\infty },A\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
26	3 25	syl	$$⊢\phi \to \left(\mathrm{-\infty },A\right]\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
27	24 26	eqeltrd	$$⊢\phi \to \left\{x\in ℝ|x\le A\right\}\in \mathrm{Clsd}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
28	1 2 3 27	orrvccel	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}A\in \mathrm{dom}P$$