Metamath Proof Explorer


Theorem orvccel

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

Ref Expression
Hypotheses orvccel.1 ( 𝜑𝑆 ran sigAlgebra )
orvccel.2 ( 𝜑𝐽 ∈ Top )
orvccel.3 ( 𝜑𝑋 ∈ ( 𝑆 MblFnM ( sigaGen ‘ 𝐽 ) ) )
orvccel.4 ( 𝜑𝐴𝑉 )
orvccel.5 ( 𝜑 → { 𝑦 𝐽𝑦 𝑅 𝐴 } ∈ ( Clsd ‘ 𝐽 ) )
Assertion orvccel ( 𝜑 → ( 𝑋RV/𝑐 𝑅 𝐴 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 orvccel.1 ( 𝜑𝑆 ran sigAlgebra )
2 orvccel.2 ( 𝜑𝐽 ∈ Top )
3 orvccel.3 ( 𝜑𝑋 ∈ ( 𝑆 MblFnM ( sigaGen ‘ 𝐽 ) ) )
4 orvccel.4 ( 𝜑𝐴𝑉 )
5 orvccel.5 ( 𝜑 → { 𝑦 𝐽𝑦 𝑅 𝐴 } ∈ ( Clsd ‘ 𝐽 ) )
6 1 2 3 4 orvcval4 ( 𝜑 → ( 𝑋RV/𝑐 𝑅 𝐴 ) = ( 𝑋 “ { 𝑦 𝐽𝑦 𝑅 𝐴 } ) )
7 2 sgsiga ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ran sigAlgebra )
8 cldssbrsiga ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
9 2 8 syl ( 𝜑 → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
10 9 5 sseldd ( 𝜑 → { 𝑦 𝐽𝑦 𝑅 𝐴 } ∈ ( sigaGen ‘ 𝐽 ) )
11 1 7 3 10 mbfmcnvima ( 𝜑 → ( 𝑋 “ { 𝑦 𝐽𝑦 𝑅 𝐴 } ) ∈ 𝑆 )
12 6 11 eqeltrd ( 𝜑 → ( 𝑋RV/𝑐 𝑅 𝐴 ) ∈ 𝑆 )