Theorem orvcval2

Description: Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		orvcval.1	⊢ ( 𝜑 → Fun 𝑋 )
2		orvcval.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
3		orvcval.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
4	1 2 3	orvcval	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) )
5		funfn	⊢ ( Fun 𝑋 ↔ 𝑋 Fn dom 𝑋 )
6	1 5	sylib	⊢ ( 𝜑 → 𝑋 Fn dom 𝑋 )
7		fncnvima2	⊢ ( 𝑋 Fn dom 𝑋 → ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) = { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) ∈ { 𝑦 ∣ 𝑦 𝑅 𝐴 } } )
8	6 7	syl	⊢ ( 𝜑 → ( ◡ 𝑋 “ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ) = { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) ∈ { 𝑦 ∣ 𝑦 𝑅 𝐴 } } )
9		fvex	⊢ ( 𝑋 ‘ 𝑧 ) ∈ V
10		breq1	⊢ ( 𝑦 = ( 𝑋 ‘ 𝑧 ) → ( 𝑦 𝑅 𝐴 ↔ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 ) )
11	9 10	elab	⊢ ( ( 𝑋 ‘ 𝑧 ) ∈ { 𝑦 ∣ 𝑦 𝑅 𝐴 } ↔ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 )
12	11	rabbii	⊢ { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) ∈ { 𝑦 ∣ 𝑦 𝑅 𝐴 } } = { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 }
13	12	a1i	⊢ ( 𝜑 → { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) ∈ { 𝑦 ∣ 𝑦 𝑅 𝐴 } } = { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 } )
14	4 8 13	3eqtrd	⊢ ( 𝜑 → ( 𝑋 ∘RV/𝑐 𝑅 𝐴 ) = { 𝑧 ∈ dom 𝑋 ∣ ( 𝑋 ‘ 𝑧 ) 𝑅 𝐴 } )