# Metamath Proof Explorer

## 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/𝑐𝐵 ) )