orrvccel

Description: If the relation produces closed sets, preimage maps are measurable sets. (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$
	orrvccel.5	$⊢ φ \to \{y \in ℝ \| y R A\} \in Clsd (topGen (ran (.)))$
Assertion	orrvccel	$⊢ φ \to X R_{RV/c} A \in dom P$

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		orrvccel.5	$⊢ φ \to \{y \in ℝ \| y R A\} \in Clsd (topGen (ran (.)))$
5		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
6	1 5	syl	$⊢ φ \to dom P \in ⋃ ran sigAlgebra$
7		retop	$⊢ topGen (ran (.)) \in Top$
8	7	a1i	$⊢ φ \to topGen (ran (.)) \in Top$
9	1	rrvmbfm	$⊢ φ \to (X \in {RndVar}_{ℝ} (P) \leftrightarrow X \in (dom P {MblFn}_{μ} 𝔅_{ℝ}))$
10	2 9	mpbid	$⊢ φ \to X \in (dom P {MblFn}_{μ} 𝔅_{ℝ})$
11		df-brsiga	$⊢ 𝔅_{ℝ} = 𝛔 (topGen (ran (.)))$
12	11	oveq2i	$⊢ dom P {MblFn}_{μ} 𝔅_{ℝ} = dom P {MblFn}_{μ} 𝛔 (topGen (ran (.)))$
13	10 12	eleqtrdi	$⊢ φ \to X \in (dom P {MblFn}_{μ} 𝛔 (topGen (ran (.))))$
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 4	eqeltrrid	$⊢ φ \to \{y \in ⋃ topGen (ran (.)) \| y R A\} \in Clsd (topGen (ran (.)))$
18	6 8 13 3 17	orvccel	$⊢ φ \to X R_{RV/c} A \in dom P$

Metamath Proof Explorer