Metamath Proof Explorer

Theorem orrvcval4

Description: The value of the preimage mapping operator can be restricted to preimages of subsets of RR. (Contributed by Thierry Arnoux, 21-Jan-2017)

		Ref	Expression
	Hypotheses	orrvccel.1	$⊢ φ \to P \in Prob$
		orrvccel.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
		orrvccel.4	$⊢ φ \to A \in V$
	Assertion	orrvcval4	$⊢ φ \to X R_{RV/c} A = X^{-1} [\{y \in ℝ \| y R A\}]$

Proof

Step	Hyp	Ref	Expression
1		orrvccel.1	$⊢ φ \to P \in Prob$
2		orrvccel.2	$⊢ φ \to X \in {RndVar}_{ℝ} (P)$
3		orrvccel.4	$⊢ φ \to A \in V$
4		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
5	1 4	syl	$⊢ φ \to dom P \in ⋃ ran sigAlgebra$
6		retop	$⊢ topGen (ran (.)) \in Top$
7	6	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
8	1	rrvmbfm	$⊢ φ \to (X \in {RndVar}_{ℝ} (P) \leftrightarrow X \in (dom P {MblFn}_{μ} 𝔅_{ℝ}))$
9	2 8	mpbid	$⊢ φ \to X \in (dom P {MblFn}_{μ} 𝔅_{ℝ})$
10		df-brsiga	$⊢ 𝔅_{ℝ} = 𝛔 (topGen (ran (.)))$
11	10	oveq2i	$⊢ dom P {MblFn}_{μ} 𝔅_{ℝ} = dom P {MblFn}_{μ} 𝛔 (topGen (ran (.)))$
12	9 11	eleqtrdi	$⊢ φ \to X \in (dom P {MblFn}_{μ} 𝛔 (topGen (ran (.))))$
13	5 7 12 3	orvcval4	$⊢ φ \to X R_{RV/c} A = X^{-1} [\{y \in ⋃ topGen (ran (.)) \| y R A\}]$
14		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
15		rabeq	$⊢ ℝ = ⋃ topGen (ran (.)) \to \{y \in ℝ \| y R A\} = \{y \in ⋃ topGen (ran (.)) \| y R A\}$
16	14 15	ax-mp	$⊢ \{y \in ℝ \| y R A\} = \{y \in ⋃ topGen (ran (.)) \| y R A\}$
17	16	imaeq2i	$⊢ X^{-1} [\{y \in ℝ \| y R A\}] = X^{-1} [\{y \in ⋃ topGen (ran (.)) \| y R A\}]$
18	13 17	eqtr4di	$⊢ φ \to X R_{RV/c} A = X^{-1} [\{y \in ℝ \| y R A\}]$