Theorem orvclteinc

Description: Preimage maps produced by the "less than or equal to" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017)

	Ref	Expression
Hypotheses	dstfrv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
	dstfrv.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
	orvclteinc.1	$$⊢\phi \to A\in ℝ$$
	orvclteinc.2	$$⊢\phi \to B\in ℝ$$
	orvclteinc.3	$$⊢\phi \to A\le B$$
Assertion	orvclteinc	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}A\subseteq X{\le }_{\mathrm{RV/c}}B$$

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		orvclteinc.1	$$⊢\phi \to A\in ℝ$$
4		orvclteinc.2	$$⊢\phi \to B\in ℝ$$
5		orvclteinc.3	$$⊢\phi \to A\le B$$
6	1 2	rrvf2	$$⊢\phi \to X:\mathrm{dom}X⟶ℝ$$
7	6	ffund	$$⊢\phi \to \mathrm{Fun}X$$
8		simp2	$$⊢\left(\phi \wedge x\in ℝ\wedge x\le A\right)\to x\in ℝ$$
9	3	3ad2ant1	$$⊢\left(\phi \wedge x\in ℝ\wedge x\le A\right)\to A\in ℝ$$
10	4	3ad2ant1	$$⊢\left(\phi \wedge x\in ℝ\wedge x\le A\right)\to B\in ℝ$$
11		simp3	$$⊢\left(\phi \wedge x\in ℝ\wedge x\le A\right)\to x\le A$$
12	5	3ad2ant1	$$⊢\left(\phi \wedge x\in ℝ\wedge x\le A\right)\to A\le B$$
13	8 9 10 11 12	letrd	$$⊢\left(\phi \wedge x\in ℝ\wedge x\le A\right)\to x\le B$$
14	13	3expia	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(x\le A\to x\le B\right)$$
15	14	ss2rabdv	$$⊢\phi \to \left\{x\in ℝ|x\le A\right\}\subseteq \left\{x\in ℝ|x\le B\right\}$$
16		sspreima	$$⊢\left(\mathrm{Fun}X\wedge \left\{x\in ℝ|x\le A\right\}\subseteq \left\{x\in ℝ|x\le B\right\}\right)\to X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]\subseteq X^{-1}\left[\left\{x\in ℝ|x\le B\right\}\right]$$
17	7 15 16	syl2anc	$$⊢\phi \to X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]\subseteq X^{-1}\left[\left\{x\in ℝ|x\le B\right\}\right]$$
18	1 2 3	orrvcval4	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}A=X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]$$
19	1 2 4	orrvcval4	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}B=X^{-1}\left[\left\{x\in ℝ|x\le B\right\}\right]$$
20	17 18 19	3sstr4d	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}A\subseteq X{\le }_{\mathrm{RV/c}}B$$