Theorem isrrvv

Description: Elementhood to the set of real-valued random variables with respect to the probability P . (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypothesis	isrrvv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
Assertion	isrrvv	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2	1	rrvmbfm	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ) )
3		domprobsiga	⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
4	1 3	syl	⊢ ( 𝜑 → dom 𝑃 ∈ ∪ ran sigAlgebra )
5		brsigarn	⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
6		elrnsiga	⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ∈ ∪ ran sigAlgebra )
7	5 6	mp1i	⊢ ( 𝜑 → 𝔅ℝ ∈ ∪ ran sigAlgebra )
8	4 7	ismbfm	⊢ ( 𝜑 → ( 𝑋 ∈ ( dom 𝑃 MblFnM 𝔅ℝ ) ↔ ( 𝑋 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) )
9		unibrsiga	⊢ ∪ 𝔅ℝ = ℝ
10	9	oveq1i	⊢ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) = ( ℝ ↑m ∪ dom 𝑃 )
11	10	eleq2i	⊢ ( 𝑋 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) ↔ 𝑋 ∈ ( ℝ ↑m ∪ dom 𝑃 ) )
12		reex	⊢ ℝ ∈ V
13	4	uniexd	⊢ ( 𝜑 → ∪ dom 𝑃 ∈ V )
14		elmapg	⊢ ( ( ℝ ∈ V ∧ ∪ dom 𝑃 ∈ V ) → ( 𝑋 ∈ ( ℝ ↑m ∪ dom 𝑃 ) ↔ 𝑋 : ∪ dom 𝑃 ⟶ ℝ ) )
15	12 13 14	sylancr	⊢ ( 𝜑 → ( 𝑋 ∈ ( ℝ ↑m ∪ dom 𝑃 ) ↔ 𝑋 : ∪ dom 𝑃 ⟶ ℝ ) )
16	11 15	bitrid	⊢ ( 𝜑 → ( 𝑋 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) ↔ 𝑋 : ∪ dom 𝑃 ⟶ ℝ ) )
17	16	anbi1d	⊢ ( 𝜑 → ( ( 𝑋 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) )
18	2 8 17	3bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) )