Theorem rfovfvd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B , and relation R . (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$$
Assertion	rfovfvd	$$⊢\phi \to F\left(R\right)=\left(x\in A⟼\left\{y\in B|xRy\right\}\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	1 2 3	rfovd	$$⊢\phi \to AOB=\left(r\in 𝒫\left(A\times B\right)⟼\left(x\in A⟼\left\{y\in B|xry\right\}\right)\right)$$
7	5 6	syl5eq	$$⊢\phi \to F=\left(r\in 𝒫\left(A\times B\right)⟼\left(x\in A⟼\left\{y\in B|xry\right\}\right)\right)$$
8		breq	$$⊢r=R\to \left(xry\leftrightarrow xRy\right)$$
9	8	rabbidv	$$⊢r=R\to \left\{y\in B|xry\right\}=\left\{y\in B|xRy\right\}$$
10	9	mpteq2dv	$$⊢r=R\to \left(x\in A⟼\left\{y\in B|xry\right\}\right)=\left(x\in A⟼\left\{y\in B|xRy\right\}\right)$$
11	10	adantl	$$⊢\left(\phi \wedge r=R\right)\to \left(x\in A⟼\left\{y\in B|xry\right\}\right)=\left(x\in A⟼\left\{y\in B|xRy\right\}\right)$$
12	2	mptexd	$$⊢\phi \to \left(x\in A⟼\left\{y\in B|xRy\right\}\right)\in \mathrm{V}$$
13	7 11 4 12	fvmptd	$$⊢\phi \to F\left(R\right)=\left(x\in A⟼\left\{y\in B|xRy\right\}\right)$$