Metamath Proof Explorer

Theorem orrvcoel

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

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		orrvcoel.5	$⊢ φ \to \{y \in ℝ \| y R A\} \in 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 topGen (ran (.))$
18	6 8 13 3 17	orvcoel	$⊢ φ \to X R_{RV/c} A \in dom P$