Theorem fsovfvfvd

Description: Value of the operator, ( A O B ) , which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, A and B , when applied to function F and element Y . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	fsovd.fs	$$⊢O=\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(f\in \left({𝒫b}^a\right)⟼\left(y\in b⟼\left\{x\in a|y\in f\left(x\right)\right\}\right)\right)\right)$$
	fsovd.a	$$⊢\phi \to A\in V$$
	fsovd.b	$$⊢\phi \to B\in W$$
	fsovfvd.g	$$⊢G=AOB$$
	fsovfvd.f	$$⊢\phi \to F\in \left({𝒫B}^A\right)$$
	fsovfvfvd.h	$$⊢H=G\left(F\right)$$
	fsovfvfvd.y	$$⊢\phi \to Y\in B$$
Assertion	fsovfvfvd	$$⊢\phi \to H\left(Y\right)=\left\{x\in A|Y\in F\left(x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	$$⊢O=\left(a\in \mathrm{V},b\in \mathrm{V}⟼\left(f\in \left({𝒫b}^a\right)⟼\left(y\in b⟼\left\{x\in a|y\in f\left(x\right)\right\}\right)\right)\right)$$
2		fsovd.a	$$⊢\phi \to A\in V$$
3		fsovd.b	$$⊢\phi \to B\in W$$
4		fsovfvd.g	$$⊢G=AOB$$
5		fsovfvd.f	$$⊢\phi \to F\in \left({𝒫B}^A\right)$$
6		fsovfvfvd.h	$$⊢H=G\left(F\right)$$
7		fsovfvfvd.y	$$⊢\phi \to Y\in B$$
8	1 2 3 4 5	fsovfvd	$$⊢\phi \to G\left(F\right)=\left(y\in B⟼\left\{x\in A|y\in F\left(x\right)\right\}\right)$$
9	6 8	syl5eq	$$⊢\phi \to H=\left(y\in B⟼\left\{x\in A|y\in F\left(x\right)\right\}\right)$$
10		eleq1	$$⊢y=Y\to \left(y\in F\left(x\right)\leftrightarrow Y\in F\left(x\right)\right)$$
11	10	rabbidv	$$⊢y=Y\to \left\{x\in A|y\in F\left(x\right)\right\}=\left\{x\in A|Y\in F\left(x\right)\right\}$$
12	11	adantl	$$⊢\left(\phi \wedge y=Y\right)\to \left\{x\in A|y\in F\left(x\right)\right\}=\left\{x\in A|Y\in F\left(x\right)\right\}$$
13		rabexg	$$⊢A\in V\to \left\{x\in A|Y\in F\left(x\right)\right\}\in \mathrm{V}$$
14	2 13	syl	$$⊢\phi \to \left\{x\in A|Y\in F\left(x\right)\right\}\in \mathrm{V}$$
15	9 12 7 14	fvmptd	$$⊢\phi \to H\left(Y\right)=\left\{x\in A|Y\in F\left(x\right)\right\}$$