dstfrvel - Mathbox for Thierry Arnoux

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

Theorem dstfrvel 34651

Description: Elementhood of preimage maps produced by the "less than or equal to" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.)

**Hypotheses**
Ref	Expression
dstfrv.1	⊢ (𝜑 → 𝑃 ∈ Prob)
dstfrv.2	⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))
orvclteel.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
dstfrvel.1	⊢ (𝜑 → 𝐵 ∈ ∪ dom 𝑃)
dstfrvel.2	⊢ (𝜑 → (𝑋‘𝐵) ≤ 𝐴)

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

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

Step	Hyp	Ref	Expression
1		dstfrv.1	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Prob)
2		dstfrv.2	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃))
3	1, 2	rrvvf 34621	. . . . 5 ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ)
4		dstfrvel.1	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ∪ dom 𝑃)
5	3, 4	ffvelcdmd 7039	. . . 4 ⊢ (𝜑 → (𝑋‘𝐵) ∈ ℝ)
6		dstfrvel.2	. . . 4 ⊢ (𝜑 → (𝑋‘𝐵) ≤ 𝐴)
7		breq1 5103	. . . . 5 ⊢ (𝑥 = (𝑋‘𝐵) → (𝑥 ≤ 𝐴 ↔ (𝑋‘𝐵) ≤ 𝐴))
8	7	elrab 3648	. . . 4 ⊢ ((𝑋‘𝐵) ∈ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴} ↔ ((𝑋‘𝐵) ∈ ℝ ∧ (𝑋‘𝐵) ≤ 𝐴))
9	5, 6, 8	sylanbrc 584	. . 3 ⊢ (𝜑 → (𝑋‘𝐵) ∈ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴})
10	3	ffund 6674	. . . 4 ⊢ (𝜑 → Fun 𝑋)
11	1, 2	rrvdm 34623	. . . . 5 ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃)
12	4, 11	eleqtrrd 2840	. . . 4 ⊢ (𝜑 → 𝐵 ∈ dom 𝑋)
13		fvimacnv 7007	. . . 4 ⊢ ((Fun 𝑋 ∧ 𝐵 ∈ dom 𝑋) → ((𝑋‘𝐵) ∈ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴} ↔ 𝐵 ∈ (^◡𝑋 “ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴})))
14	10, 12, 13	syl2anc 585	. . 3 ⊢ (𝜑 → ((𝑋‘𝐵) ∈ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴} ↔ 𝐵 ∈ (^◡𝑋 “ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴})))
15	9, 14	mpbid 232	. 2 ⊢ (𝜑 → 𝐵 ∈ (^◡𝑋 “ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴}))
16		orvclteel.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
17	1, 2, 16	orrvcval4 34642	. 2 ⊢ (𝜑 → (𝑋∘_RV/𝑐 ≤ 𝐴) = (^◡𝑋 “ {𝑥 ∈ ℝ ∣ 𝑥 ≤ 𝐴}))
18	15, 17	eleqtrrd 2840	1 ⊢ (𝜑 → 𝐵 ∈ (𝑋∘_RV/𝑐 ≤ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2114 {crab 3401 ∪ cuni 4865 class class class wbr 5100 ^◡ccnv 5631 dom cdm 5632 “ cima 5635 Fun wfun 6494 ‘cfv 6500 (class class class)co 7368 ℝcr 11037 ≤ cle 11179 Probcprb 34584 rRndVarcrrv 34617 ∘_RV/𝑐corvc 34633

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 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-pre-lttri 11112 ax-pre-lttrn 11113

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 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-po 5540 df-so 5541 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-1st 7943 df-2nd 7944 df-er 8645 df-map 8777 df-en 8896 df-dom 8897 df-sdom 8898 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-ioo 13277 df-topgen 17375 df-top 22850 df-bases 22902 df-esum 34205 df-siga 34286 df-sigagen 34316 df-brsiga 34359 df-meas 34373 df-mbfm 34427 df-prob 34585 df-rrv 34618 df-orvc 34634

This theorem is referenced by: dstfrvunirn 34652

W3C validator