Theorem rfovfvfvd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , relation R , and left element X . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	rfovd.rf	$$⊢O=\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(r\in 𝒫\left(a\times b\right)⟼\left(x\in a⟼\left\{y\in b|xry\right\}\right)\right)\right)$$
	rfovd.a	$$⊢\phi \to A\in V$$
	rfovd.b	$$⊢\phi \to B\in W$$
	rfovfvd.r	$$⊢\phi \to R\in 𝒫\left(A\times B\right)$$
	rfovfvd.f	$$⊢F=AOB$$
	rfovfvfvd.x	$$⊢\phi \to X\in A$$
	rfovfvfvd.g	$$⊢G=F\left(R\right)$$
Assertion	rfovfvfvd	$$⊢\phi \to G\left(X\right)=\left\{y\in B|XRy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	$$⊢O=\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(r\in 𝒫\left(a\times b\right)⟼\left(x\in a⟼\left\{y\in b|xry\right\}\right)\right)\right)$$
2		rfovd.a	$$⊢\phi \to A\in V$$
3		rfovd.b	$$⊢\phi \to B\in W$$
4		rfovfvd.r	$$⊢\phi \to R\in 𝒫\left(A\times B\right)$$
5		rfovfvd.f	$$⊢F=AOB$$
6		rfovfvfvd.x	$$⊢\phi \to X\in A$$
7		rfovfvfvd.g	$$⊢G=F\left(R\right)$$
8	1 2 3 4 5	rfovfvd	$$⊢\phi \to F\left(R\right)=\left(x\in A⟼\left\{y\in B|xRy\right\}\right)$$
9	7 8	syl5eq	$$⊢\phi \to G=\left(x\in A⟼\left\{y\in B|xRy\right\}\right)$$
10		breq1	$$⊢x=X\to \left(xRy\leftrightarrow XRy\right)$$
11	10	rabbidv	$$⊢x=X\to \left\{y\in B|xRy\right\}=\left\{y\in B|XRy\right\}$$
12	11	adantl	$$⊢\left(\phi \wedge x=X\right)\to \left\{y\in B|xRy\right\}=\left\{y\in B|XRy\right\}$$
13		rabexg	$$⊢B\in W\to \left\{y\in B|XRy\right\}\in \mathrm{V}$$
14	3 13	syl	$$⊢\phi \to \left\{y\in B|XRy\right\}\in \mathrm{V}$$
15	9 12 6 14	fvmptd	$$⊢\phi \to G\left(X\right)=\left\{y\in B|XRy\right\}$$