Theorem orvcelval

Description: Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dstrvprob.1	⊢ ( 𝜑 → 𝑃 ∈ Prob )
2		dstrvprob.2	⊢ ( 𝜑 → 𝑋 ∈ ( rRndVar ‘ 𝑃 ) )
3		orvcelel.1	⊢ ( 𝜑 → 𝐴 ∈ 𝔅ℝ )
4	1 2 3	orrvcval4	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 E 𝐴 ) = ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 E 𝐴 } ) )
5		epelg	⊢ ( 𝐴 ∈ 𝔅ℝ → ( 𝑥 E 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝑥 E 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
7	6	rabbidv	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 E 𝐴 } = { 𝑥 ∈ ℝ ∣ 𝑥 ∈ 𝐴 } )
8		dfin5	⊢ ( ℝ ∩ 𝐴 ) = { 𝑥 ∈ ℝ ∣ 𝑥 ∈ 𝐴 }
9	8	a1i	⊢ ( 𝜑 → ( ℝ ∩ 𝐴 ) = { 𝑥 ∈ ℝ ∣ 𝑥 ∈ 𝐴 } )
10		elssuni	⊢ ( 𝐴 ∈ 𝔅ℝ → 𝐴 ⊆ ∪ 𝔅ℝ )
11		unibrsiga	⊢ ∪ 𝔅ℝ = ℝ
12	10 11	sseqtrdi	⊢ ( 𝐴 ∈ 𝔅ℝ → 𝐴 ⊆ ℝ )
13	3 12	syl	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
14		sseqin2	⊢ ( 𝐴 ⊆ ℝ ↔ ( ℝ ∩ 𝐴 ) = 𝐴 )
15	13 14	sylib	⊢ ( 𝜑 → ( ℝ ∩ 𝐴 ) = 𝐴 )
16	7 9 15	3eqtr2d	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ 𝑥 E 𝐴 } = 𝐴 )
17	16	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑥 ∈ ℝ ∣ 𝑥 E 𝐴 } ) = ( ◡ 𝑋 “ 𝐴 ) )
18	4 17	eqtrd	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 E 𝐴 ) = ( ◡ 𝑋 “ 𝐴 ) )