Theorem rrvmbfm

Description: A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypothesis	isrrvv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
Assertion	rrvmbfm	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dmeq	⊢ ( 𝑝 = 𝑃 → dom 𝑝 = dom 𝑃 )
3	2	oveq1d	⊢ ( 𝑝 = 𝑃 → ( dom 𝑝 MblFnM 𝔅ℝ ) = ( dom 𝑃 MblFnM 𝔅ℝ ) )
4		df-rrv	⊢ rRndVar = ( 𝑝 ∈ Prob ↦ ( dom 𝑝 MblFnM 𝔅ℝ ) )
5		ovex	⊢ ( dom 𝑃 MblFnM 𝔅ℝ ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝑃 ∈ Prob → ( rRndVar ‘ 𝑃 ) = ( dom 𝑃 MblFnM 𝔅ℝ ) )
7	1 6	syl	⊢ ( 𝜑 → ( rRndVar ‘ 𝑃 ) = ( dom 𝑃 MblFnM 𝔅ℝ ) )
8	7	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )