Theorem dstfrvinc

Description: A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017)

	Ref	Expression
Hypotheses	dstfrv.1	|- ( ph -> P e. Prob )
	dstfrv.2	|- ( ph -> X e. ( rRndVar ` P ) )
	dstfrv.3	|- ( ph -> F = ( x e. RR |-> ( P ` ( X oRVC <_ x ) ) ) )
	dstfrvinc.1	|- ( ph -> A e. RR )
	dstfrvinc.2	|- ( ph -> B e. RR )
	dstfrvinc.3	|- ( ph -> A <_ B )
Assertion	dstfrvinc	|- ( ph -> ( F ` A ) <_ ( F ` B ) )

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	|- ( ph -> P e. Prob )
2		dstfrv.2	|- ( ph -> X e. ( rRndVar ` P ) )
3		dstfrv.3	|- ( ph -> F = ( x e. RR |-> ( P ` ( X oRVC <_ x ) ) ) )
4		dstfrvinc.1	|- ( ph -> A e. RR )
5		dstfrvinc.2	|- ( ph -> B e. RR )
6		dstfrvinc.3	|- ( ph -> A <_ B )
7		domprobmeas	|- ( P e. Prob -> P e. ( measures ` dom P ) )
8	1 7	syl	|- ( ph -> P e. ( measures ` dom P ) )
9	1 2 4	orvclteel	|- ( ph -> ( X oRVC <_ A ) e. dom P )
10	1 2 5	orvclteel	|- ( ph -> ( X oRVC <_ B ) e. dom P )
11	1 2 4 5 6	orvclteinc	|- ( ph -> ( X oRVC <_ A ) C_ ( X oRVC <_ B ) )
12	8 9 10 11	measssd	|- ( ph -> ( P ` ( X oRVC <_ A ) ) <_ ( P ` ( X oRVC <_ B ) ) )
13		simpr	|- ( ( ph /\ x = A ) -> x = A )
14	13	oveq2d	|- ( ( ph /\ x = A ) -> ( X oRVC <_ x ) = ( X oRVC <_ A ) )
15	14	fveq2d	|- ( ( ph /\ x = A ) -> ( P ` ( X oRVC <_ x ) ) = ( P ` ( X oRVC <_ A ) ) )
16	1 9	probvalrnd	|- ( ph -> ( P ` ( X oRVC <_ A ) ) e. RR )
17	3 15 4 16	fvmptd	|- ( ph -> ( F ` A ) = ( P ` ( X oRVC <_ A ) ) )
18		simpr	|- ( ( ph /\ x = B ) -> x = B )
19	18	oveq2d	|- ( ( ph /\ x = B ) -> ( X oRVC <_ x ) = ( X oRVC <_ B ) )
20	19	fveq2d	|- ( ( ph /\ x = B ) -> ( P ` ( X oRVC <_ x ) ) = ( P ` ( X oRVC <_ B ) ) )
21	1 10	probvalrnd	|- ( ph -> ( P ` ( X oRVC <_ B ) ) e. RR )
22	3 20 5 21	fvmptd	|- ( ph -> ( F ` B ) = ( P ` ( X oRVC <_ B ) ) )
23	12 17 22	3brtr4d	|- ( ph -> ( F ` A ) <_ ( F ` B ) )