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	|- ( ph -> P e. Prob )
	dstfrv.2	|- ( ph -> X e. ( rRndVar ` P ) )
	orvclteinc.1	|- ( ph -> A e. RR )
	orvclteinc.2	|- ( ph -> B e. RR )
	orvclteinc.3	|- ( ph -> A <_ B )
Assertion	orvclteinc	|- ( ph -> ( X oRVC <_ A ) C_ ( X oRVC <_ B ) )

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	|- ( ph -> P e. Prob )
2		dstfrv.2	|- ( ph -> X e. ( rRndVar ` P ) )
3		orvclteinc.1	|- ( ph -> A e. RR )
4		orvclteinc.2	|- ( ph -> B e. RR )
5		orvclteinc.3	|- ( ph -> A <_ B )
6	1 2	rrvf2	|- ( ph -> X : dom X --> RR )
7	6	ffund	|- ( ph -> Fun X )
8		simp2	|- ( ( ph /\ x e. RR /\ x <_ A ) -> x e. RR )
9	3	3ad2ant1	|- ( ( ph /\ x e. RR /\ x <_ A ) -> A e. RR )
10	4	3ad2ant1	|- ( ( ph /\ x e. RR /\ x <_ A ) -> B e. RR )
11		simp3	|- ( ( ph /\ x e. RR /\ x <_ A ) -> x <_ A )
12	5	3ad2ant1	|- ( ( ph /\ x e. RR /\ x <_ A ) -> A <_ B )
13	8 9 10 11 12	letrd	|- ( ( ph /\ x e. RR /\ x <_ A ) -> x <_ B )
14	13	3expia	|- ( ( ph /\ x e. RR ) -> ( x <_ A -> x <_ B ) )
15	14	ss2rabdv	|- ( ph -> { x e. RR | x <_ A } C_ { x e. RR | x <_ B } )
16		sspreima	|- ( ( Fun X /\ { x e. RR | x <_ A } C_ { x e. RR | x <_ B } ) -> ( `' X " { x e. RR | x <_ A } ) C_ ( `' X " { x e. RR | x <_ B } ) )
17	7 15 16	syl2anc	|- ( ph -> ( `' X " { x e. RR | x <_ A } ) C_ ( `' X " { x e. RR | x <_ B } ) )
18	1 2 3	orrvcval4	|- ( ph -> ( X oRVC <_ A ) = ( `' X " { x e. RR | x <_ A } ) )
19	1 2 4	orrvcval4	|- ( ph -> ( X oRVC <_ B ) = ( `' X " { x e. RR | x <_ B } ) )
20	17 18 19	3sstr4d	|- ( ph -> ( X oRVC <_ A ) C_ ( X oRVC <_ B ) )