# Metamath Proof Explorer

## Theorem dstfrvinc

Description: A cumulative distribution function is nondecreasing. (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)$
dstfrv.3 ${⊢}{\phi }\to {F}=\left({x}\in ℝ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)\right)$
dstfrvinc.1 ${⊢}{\phi }\to {A}\in ℝ$
dstfrvinc.2 ${⊢}{\phi }\to {B}\in ℝ$
dstfrvinc.3 ${⊢}{\phi }\to {A}\le {B}$
Assertion dstfrvinc ${⊢}{\phi }\to {F}\left({A}\right)\le {F}\left({B}\right)$

### 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 dstfrv.3 ${⊢}{\phi }\to {F}=\left({x}\in ℝ⟼{P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)\right)$
4 dstfrvinc.1 ${⊢}{\phi }\to {A}\in ℝ$
5 dstfrvinc.2 ${⊢}{\phi }\to {B}\in ℝ$
6 dstfrvinc.3 ${⊢}{\phi }\to {A}\le {B}$
7 domprobmeas ${⊢}{P}\in \mathrm{Prob}\to {P}\in \mathrm{measures}\left(\mathrm{dom}{P}\right)$
8 1 7 syl ${⊢}{\phi }\to {P}\in \mathrm{measures}\left(\mathrm{dom}{P}\right)$
9 1 2 4 orvclteel ${⊢}{\phi }\to {X}{\le }_{\mathrm{RV/c}}{A}\in \mathrm{dom}{P}$
10 1 2 5 orvclteel ${⊢}{\phi }\to {X}{\le }_{\mathrm{RV/c}}{B}\in \mathrm{dom}{P}$
11 1 2 4 5 6 orvclteinc ${⊢}{\phi }\to {X}{\le }_{\mathrm{RV/c}}{A}\subseteq {X}{\le }_{\mathrm{RV/c}}{B}$
12 8 9 10 11 measssd ${⊢}{\phi }\to {P}\left({X}{\le }_{\mathrm{RV/c}}{A}\right)\le {P}\left({X}{\le }_{\mathrm{RV/c}}{B}\right)$
13 simpr ${⊢}\left({\phi }\wedge {x}={A}\right)\to {x}={A}$
14 13 oveq2d ${⊢}\left({\phi }\wedge {x}={A}\right)\to {X}{\le }_{\mathrm{RV/c}}{x}={X}{\le }_{\mathrm{RV/c}}{A}$
15 14 fveq2d ${⊢}\left({\phi }\wedge {x}={A}\right)\to {P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{A}\right)$
16 1 9 probvalrnd ${⊢}{\phi }\to {P}\left({X}{\le }_{\mathrm{RV/c}}{A}\right)\in ℝ$
17 3 15 4 16 fvmptd ${⊢}{\phi }\to {F}\left({A}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{A}\right)$
18 simpr ${⊢}\left({\phi }\wedge {x}={B}\right)\to {x}={B}$
19 18 oveq2d ${⊢}\left({\phi }\wedge {x}={B}\right)\to {X}{\le }_{\mathrm{RV/c}}{x}={X}{\le }_{\mathrm{RV/c}}{B}$
20 19 fveq2d ${⊢}\left({\phi }\wedge {x}={B}\right)\to {P}\left({X}{\le }_{\mathrm{RV/c}}{x}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{B}\right)$
21 1 10 probvalrnd ${⊢}{\phi }\to {P}\left({X}{\le }_{\mathrm{RV/c}}{B}\right)\in ℝ$
22 3 20 5 21 fvmptd ${⊢}{\phi }\to {F}\left({B}\right)={P}\left({X}{\le }_{\mathrm{RV/c}}{B}\right)$
23 12 17 22 3brtr4d ${⊢}{\phi }\to {F}\left({A}\right)\le {F}\left({B}\right)$