Metamath Proof Explorer

Theorem orrvccel

Description: If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orrvccel.1 ⊢ φ → P ∈ Prob
orrvccel.2 ⊢ φ → X ∈ RndVar ℝ ⁡ P
orrvccel.4 ⊢ φ → A ∈ V
orrvccel.5 ⊢ φ → y ∈ ℝ | y R A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
Assertion orrvccel ⊢ φ → X R RV/c A ∈ dom ⁡ P

Proof

Step Hyp Ref Expression
1 orrvccel.1 ⊢ φ → P ∈ Prob
2 orrvccel.2 ⊢ φ → X ∈ RndVar ℝ ⁡ P
3 orrvccel.4 ⊢ φ → A ∈ V
4 orrvccel.5 ⊢ φ → y ∈ ℝ | y R A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
5 domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
6 1 5 syl ⊢ φ → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
7 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
8 7 a1i ⊢ φ → topGen ⁡ ran ⁡ . ∈ Top
9 1 rrvmbfm ⊢ φ → X ∈ RndVar ℝ ⁡ P ↔ X ∈ dom ⁡ P MblFn μ 𝔅 ℝ
10 2 9 mpbid ⊢ φ → X ∈ dom ⁡ P MblFn μ 𝔅 ℝ
11 df-brsiga ⊢ 𝔅 ℝ = 𝛔 ⁡ topGen ⁡ ran ⁡ .
12 11 oveq2i ⊢ dom ⁡ P MblFn μ 𝔅 ℝ = dom ⁡ P MblFn μ 𝛔 ⁡ topGen ⁡ ran ⁡ .
13 10 12 eleqtrdi ⊢ φ → X ∈ dom ⁡ P MblFn μ 𝛔 ⁡ topGen ⁡ ran ⁡ .
14 uniretop ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .
15 rabeq ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ . → y ∈ ℝ | y R A = y ∈ ⋃ topGen ⁡ ran ⁡ . | y R A
16 14 15 ax-mp ⊢ y ∈ ℝ | y R A = y ∈ ⋃ topGen ⁡ ran ⁡ . | y R A
17 16 4 eqeltrrid ⊢ φ → y ∈ ⋃ topGen ⁡ ran ⁡ . | y R A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .
18 6 8 13 3 17 orvccel ⊢ φ → X R RV/c A ∈ dom ⁡ P