orvclteinc - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > orvclteinc		Structured version Visualization version GIF version

Theorem orvclteinc 34636

Description: Preimage maps produced by the "less than or equal to" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.)

**Hypotheses**
Ref	Expression
dstfrv.1	⊢ (𝜑 → 𝑃 ∈ Prob)
dstfrv.2	⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))
orvclteinc.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
orvclteinc.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
orvclteinc.3	⊢ (𝜑 → 𝐴 ≤ 𝐵)

**Assertion**
Ref	Expression
orvclteinc	⊢ (𝜑 → (𝑋∘_RV/𝑐 ≤ 𝐴) ⊆ (𝑋∘_RV/𝑐 ≤ 𝐵))

Proof of Theorem orvclteinc Dummy variable 𝑥 is distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1087 ∈ wcel 2114 {crab 3390 ⊆ wss 3890 class class class wbr 5086 ^◡ccnv 5623 dom cdm 5624 “ cima 5627 Fun wfun 6486 ‘cfv 6492 (class class class)co 7360 ℝcr 11028 ≤ cle 11171 Probcprb 34567 rRndVarcrrv 34600 ∘_RV/𝑐corvc 34616

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-pre-lttri 11103 ax-pre-lttrn 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-po 5532 df-so 5533 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-1st 7935 df-2nd 7936 df-er 8636 df-map 8768 df-en 8887 df-dom 8888 df-sdom 8889 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-ioo 13293 df-topgen 17397 df-top 22869 df-bases 22921 df-esum 34188 df-siga 34269 df-sigagen 34299 df-brsiga 34342 df-meas 34356 df-mbfm 34410 df-prob 34568 df-rrv 34601 df-orvc 34617

This theorem is referenced by: dstfrvinc 34637 dstfrvclim1 34638

W3C validator