Metamath Proof Explorer


Theorem orvcoel

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

Ref Expression
Hypotheses orvccel.1 φ S ran sigAlgebra
orvccel.2 φ J Top
orvccel.3 φ X S MblFn μ 𝛔 J
orvccel.4 φ A V
orvcoel.5 φ y J | y R A J
Assertion orvcoel φ X R RV/c A S

Proof

Step Hyp Ref Expression
1 orvccel.1 φ S ran sigAlgebra
2 orvccel.2 φ J Top
3 orvccel.3 φ X S MblFn μ 𝛔 J
4 orvccel.4 φ A V
5 orvcoel.5 φ y J | y R A J
6 1 2 3 4 orvcval4 φ X R RV/c A = X -1 y J | y R A
7 2 sgsiga φ 𝛔 J ran sigAlgebra
8 sssigagen J Top J 𝛔 J
9 2 8 syl φ J 𝛔 J
10 9 5 sseldd φ y J | y R A 𝛔 J
11 1 7 3 10 mbfmcnvima φ X -1 y J | y R A S
12 6 11 eqeltrd φ X R RV/c A S