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)$$