# Metamath Proof Explorer

## 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}$