Theorem orvcval

Description: Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017)

	Ref	Expression
Hypotheses	orvcval.1	⊢ ( 𝜑 → Fun 𝑋 )
	orvcval.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	orvcval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
Assertion	orvcval	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		orvcval.1	⊢ ( 𝜑 → Fun 𝑋 )
2		orvcval.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
3		orvcval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
4		df-orvc	⊢ ∘RV/𝑐 𝑅 = ( 𝑥 ∈ { 𝑥 ∣ Fun 𝑥 } , 𝑎 ∈ V ↦ ( ◡ 𝑥 “ { 𝑦 ∣ 𝑦 𝑅 𝑎 } ) )
5	4	a1i	⊢ ( 𝜑 → ∘RV/𝑐 𝑅 = ( 𝑥 ∈ { 𝑥 ∣ Fun 𝑥 } , 𝑎 ∈ V ↦ ( ◡ 𝑥 “ { 𝑦 ∣ 𝑦 𝑅 𝑎 } ) ) )
6		simpl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) → 𝑥 = 𝑋 )
7	6	cnveqd	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) → ◡ 𝑥 = ◡ 𝑋 )
8		simpr	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
9	8	breq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) → ( 𝑦 𝑅 𝑎 ↔ 𝑦 𝑅 𝐴 ) )
10	9	abbidv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) → { 𝑦 ∣ 𝑦 𝑅 𝑎 } = { 𝑦 ∣ 𝑦 𝑅 𝐴 } )
11	7 10	imaeq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) → ( ◡ 𝑥 “ { 𝑦 ∣ 𝑦 𝑅 𝑎 } ) = ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑎 = 𝐴 ) ) → ( ◡ 𝑥 “ { 𝑦 ∣ 𝑦 𝑅 𝑎 } ) = ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) )
13		funeq	⊢ ( 𝑥 = 𝑋 → ( Fun 𝑥 ↔ Fun 𝑋 ) )
14	2 1 13	elabd	⊢ ( 𝜑 → 𝑋 ∈ { 𝑥 ∣ Fun 𝑥 } )
15		elex	⊢ ( 𝐴 ∈ 𝑊 → 𝐴 ∈ V )
16	3 15	syl	⊢ ( 𝜑 → 𝐴 ∈ V )
17		cnvexg	⊢ ( 𝑋 ∈ 𝑉 → ◡ 𝑋 ∈ V )
18		imaexg	⊢ ( ◡ 𝑋 ∈ V → ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) ∈ V )
19	2 17 18	3syl	⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) ∈ V )
20	5 12 14 16 19	ovmpod	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) )