Theorem orvcelel

Description: Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017)

	Ref	Expression
Hypotheses	dstrvprob.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
	dstrvprob.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
	orvcelel.1	⊢ ( 𝜑 → 𝐴 ∈ 𝔅ℝ )
Assertion	orvcelel	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 E 𝐴 ) ∈ dom 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dstrvprob.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orvcelel.1	⊢ ( 𝜑 → 𝐴 ∈ 𝔅ℝ )
4	1 2 3	orvcelval	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 E 𝐴 ) = ( ◡ 𝑋 “ 𝐴 ) )
5	1 2	rrvfinvima	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑎 ) ∈ dom 𝑃 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
7	6	imaeq2d	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( ◡ 𝑋 “ 𝑎 ) = ( ◡ 𝑋 “ 𝐴 ) )
8	7	eleq1d	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( ( ◡ 𝑋 “ 𝑎 ) ∈ dom 𝑃 ↔ ( ◡ 𝑋 “ 𝐴 ) ∈ dom 𝑃 ) )
9	3 8	rspcdv	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ 𝔅ℝ ( ◡ 𝑋 “ 𝑎 ) ∈ dom 𝑃 → ( ◡ 𝑋 “ 𝐴 ) ∈ dom 𝑃 ) )
10	5 9	mpd	⊢ ( 𝜑 → ( ◡ 𝑋 “ 𝐴 ) ∈ dom 𝑃 )
11	4 10	eqeltrd	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 E 𝐴 ) ∈ dom 𝑃 )