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
|
syl5bb |
⊢ ( 𝜑 → ( 𝑋 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) ↔ 𝑋 : ∪ dom 𝑃 ⟶ ℝ ) ) |
17 |
16
|
anbi1d |
⊢ ( 𝜑 → ( ( 𝑋 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom 𝑃 ) ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) ) |
18 |
2 8 17
|
3bitrd |
⊢ ( 𝜑 → ( 𝑋 ∈ ( rRndVar ‘ 𝑃 ) ↔ ( 𝑋 : ∪ dom 𝑃 ⟶ ℝ ∧ ∀ 𝑦 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑦 ) ∈ dom 𝑃 ) ) ) |