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	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	orrvccel.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	orrvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	orrvcval4	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∈ ℝ ∣ 𝑦 𝑅 𝐴 } ) )

Proof

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