Theorem dstfrvel

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

	Ref	Expression
Hypotheses	dstfrv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
	dstfrv.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
	orvclteel.1	$$⊢\phi \to A\in ℝ$$
	dstfrvel.1	$$⊢\phi \to B\in \bigcup \mathrm{dom}P$$
	dstfrvel.2	$$⊢\phi \to X\left(B\right)\le A$$
Assertion	dstfrvel	$$⊢\phi \to B\in \left(X{\le }_{\mathrm{RV/c}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dstfrv.1	$$⊢\phi \to P\in \mathrm{Prob}$$
2		dstfrv.2	$$⊢\phi \to X\in {\mathrm{RndVar}}_{ℝ}\left(P\right)$$
3		orvclteel.1	$$⊢\phi \to A\in ℝ$$
4		dstfrvel.1	$$⊢\phi \to B\in \bigcup \mathrm{dom}P$$
5		dstfrvel.2	$$⊢\phi \to X\left(B\right)\le A$$
6	1 2	rrvvf	$$⊢\phi \to X:\bigcup \mathrm{dom}P⟶ℝ$$
7	6 4	ffvelrnd	$$⊢\phi \to X\left(B\right)\in ℝ$$
8		breq1	$$⊢x=X\left(B\right)\to \left(x\le A\leftrightarrow X\left(B\right)\le A\right)$$
9	8	elrab	$$⊢X\left(B\right)\in \left\{x\in ℝ|x\le A\right\}\leftrightarrow \left(X\left(B\right)\in ℝ\wedge X\left(B\right)\le A\right)$$
10	7 5 9	sylanbrc	$$⊢\phi \to X\left(B\right)\in \left\{x\in ℝ|x\le A\right\}$$
11	6	ffund	$$⊢\phi \to \mathrm{Fun}X$$
12	1 2	rrvdm	$$⊢\phi \to \mathrm{dom}X=\bigcup \mathrm{dom}P$$
13	4 12	eleqtrrd	$$⊢\phi \to B\in \mathrm{dom}X$$
14		fvimacnv	$$⊢\left(\mathrm{Fun}X\wedge B\in \mathrm{dom}X\right)\to \left(X\left(B\right)\in \left\{x\in ℝ|x\le A\right\}\leftrightarrow B\in X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]\right)$$
15	11 13 14	syl2anc	$$⊢\phi \to \left(X\left(B\right)\in \left\{x\in ℝ|x\le A\right\}\leftrightarrow B\in X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]\right)$$
16	10 15	mpbid	$$⊢\phi \to B\in X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]$$
17	1 2 3	orrvcval4	$$⊢\phi \to X{\le }_{\mathrm{RV/c}}A=X^{-1}\left[\left\{x\in ℝ|x\le A\right\}\right]$$
18	16 17	eleqtrrd	$$⊢\phi \to B\in \left(X{\le }_{\mathrm{RV/c}}A\right)$$