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	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	dstfrv.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	orvclteinc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	orvclteinc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	orvclteinc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
Assertion	orvclteinc	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ≤ 𝐴 ) ⊆ ( 𝑋 ∘RV/𝑐 ≤ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dstfrv.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orvclteinc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4		orvclteinc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5		orvclteinc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
6	1 2	rrvf2	⊢ ( 𝜑 → 𝑋 : dom 𝑋 ⟶ ℝ )
7	6	ffund	⊢ ( 𝜑 → Fun 𝑋 )
8		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) → 𝑥 ∈ ℝ )
9	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
10	4	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) → 𝐵 ∈ ℝ )
11		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) → 𝑥 ≤ 𝐴 )
12	5	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) → 𝐴 ≤ 𝐵 )
13	8 9 10 11 12	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝐴 ) → 𝑥 ≤ 𝐵 )
14	13	3expia	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ≤ 𝐴 → 𝑥 ≤ 𝐵 ) )
15	14	ss2rabdv	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } ⊆ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐵 } )
16		sspreima	⊢ ( ( Fun 𝑋 ∧ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } ⊆ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐵 } ) → ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } ) ⊆ ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐵 } ) )
17	7 15 16	syl2anc	⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } ) ⊆ ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐵 } ) )
18	1 2 3	orrvcval4	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ≤ 𝐴 ) = ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴 } ) )
19	1 2 4	orrvcval4	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ≤ 𝐵 ) = ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐵 } ) )
20	17 18 19	3sstr4d	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 ≤ 𝐴 ) ⊆ ( 𝑋 ∘RV/𝑐 ≤ 𝐵 ) )