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

Proof

Step	Hyp	Ref	Expression
1		orrvccel.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		orrvccel.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orrvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		orrvccel.5	⊢ ( 𝜑 → { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ∈ ( Clsd ‘ ( 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 (,) ) ∣ 𝑦 𝑅 𝐴 } ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
18	6 8 13 3 17	orvccel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ∈ dom 𝑃 )