Metamath Proof Explorer

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	$⊢ φ \to P \in Prob$
	Assertion	isrrvv	$⊢ φ \to (X \in {RndVar}_{ℝ} (P) \leftrightarrow (X : ⋃ dom P ⟶ ℝ \land \forall y \in 𝔅_{ℝ} X^{-1} [y] \in dom P))$

Proof

Step	Hyp	Ref	Expression
1		isrrvv.1	$⊢ φ \to P \in Prob$
2	1	rrvmbfm	$⊢ φ \to (X \in {RndVar}_{ℝ} (P) \leftrightarrow X \in (dom P {MblFn}_{μ} 𝔅_{ℝ}))$
3		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
4	1 3	syl	$⊢ φ \to dom P \in ⋃ ran sigAlgebra$
5		brsigarn	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ)$
6		elrnsiga	$⊢ 𝔅_{ℝ} \in sigAlgebra (ℝ) \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
7	5 6	mp1i	$⊢ φ \to 𝔅_{ℝ} \in ⋃ ran sigAlgebra$
8	4 7	ismbfm	$⊢ φ \to (X \in (dom P {MblFn}_{μ} 𝔅_{ℝ}) \leftrightarrow (X \in ({⋃ 𝔅_{ℝ}}^{⋃ dom P}) \land \forall y \in 𝔅_{ℝ} X^{-1} [y] \in dom P))$
9		unibrsiga	$⊢ ⋃ 𝔅_{ℝ} = ℝ$
10	9	oveq1i	$⊢ {⋃ 𝔅_{ℝ}}^{⋃ dom P} = ℝ^{⋃ dom P}$
11	10	eleq2i	$⊢ X \in ({⋃ 𝔅_{ℝ}}^{⋃ dom P}) \leftrightarrow X \in (ℝ^{⋃ dom P})$
12		reex	$⊢ ℝ \in V$
13	4	uniexd	$⊢ φ \to ⋃ dom P \in V$
14		elmapg	$⊢ (ℝ \in V \land ⋃ dom P \in V) \to (X \in (ℝ^{⋃ dom P}) \leftrightarrow X : ⋃ dom P ⟶ ℝ)$
15	12 13 14	sylancr	$⊢ φ \to (X \in (ℝ^{⋃ dom P}) \leftrightarrow X : ⋃ dom P ⟶ ℝ)$
16	11 15	bitrid	$⊢ φ \to (X \in ({⋃ 𝔅_{ℝ}}^{⋃ dom P}) \leftrightarrow X : ⋃ dom P ⟶ ℝ)$
17	16	anbi1d	$⊢ φ \to ((X \in ({⋃ 𝔅_{ℝ}}^{⋃ dom P}) \land \forall y \in 𝔅_{ℝ} X^{-1} [y] \in dom P) \leftrightarrow (X : ⋃ dom P ⟶ ℝ \land \forall y \in 𝔅_{ℝ} X^{-1} [y] \in dom P))$
18	2 8 17	3bitrd	$⊢ φ \to (X \in {RndVar}_{ℝ} (P) \leftrightarrow (X : ⋃ dom P ⟶ ℝ \land \forall y \in 𝔅_{ℝ} X^{-1} [y] \in dom P))$