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	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
	orvccel.2	⊢ ( 𝜑 → 𝐽 ∈ Top )
	orvccel.3	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 MblFnM ( sigaGen ‘ 𝐽 ) ) )
	orvccel.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	orvcoel.5	⊢ ( 𝜑 → { 𝑦 ∈ ∪ 𝐽 ∣ 𝑦 𝑅 𝐴 } ∈ 𝐽 )
Assertion	orvcoel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) ∈ 𝑆 )

Proof

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