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	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	orrvccel.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	orrvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	orrvcoel.5	⊢ ( 𝜑 → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ∈ ( topGen ‘ ran (,) ) )
Assertion	orrvcoel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ∈ dom 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		orrvccel.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		orrvccel.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orrvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		orrvcoel.5	⊢ ( 𝜑 → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ∈ ( topGen ‘ ran (,) ) )
5		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
6	1 5	syl	⊢ ( 𝜑 → dom 𝑃 ∈ ∪ ran sigAlgebra )
7		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
8	7	a1i	⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
9	1	rrvmbfm	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
10	2 9	mpbid	⊢ ( 𝜑 → 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) )
11		df-brsiga	⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
12	11	oveq2i	⊢ ( dom 𝑃 MblFnM 𝔅ℝ ) = ( dom 𝑃 MblFnM ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
13	10 12	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( dom 𝑃 MblFnM ( sigaGen ‘ ( topGen ‘ ran (,) ) ) ) )
14		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
15		rabeq	⊢ ( ℝ = ∪ ( topGen ‘ ran (,) ) → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } = { 𝑦 ∈ ∪ ( topGen ‘ ran (,) ) ∣ 𝑦 𝑅 𝐴 } )
16	14 15	ax-mp	⊢ { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } = { 𝑦 ∈ ∪ ( topGen ‘ ran (,) ) ∣ 𝑦 𝑅 𝐴 }
17	16 4	eqeltrrid	⊢ ( 𝜑 → { 𝑦 ∈ ∪ ( topGen ‘ ran (,) ) ∣ 𝑦 𝑅 𝐴 } ∈ ( topGen ‘ ran (,) ) )
18	6 8 13 3 17	orvcoel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ∈ dom 𝑃 )