Theorem fsovd

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 . (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$$
Assertion	fsovd	$$⊢\phi \to AOB=\left(f\in \left({𝒫B}^A\right)⟼\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\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	1	a1i	$$⊢\phi \to 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)$$
5		pweq	$$⊢b=B\to 𝒫b=𝒫B$$
6	5	adantl	$$⊢\left(a=A\wedge b=B\right)\to 𝒫b=𝒫B$$
7		simpl	$$⊢\left(a=A\wedge b=B\right)\to a=A$$
8	6 7	oveq12d	$$⊢\left(a=A\wedge b=B\right)\to {𝒫b}^a={𝒫B}^A$$
9		simpr	$$⊢\left(a=A\wedge b=B\right)\to b=B$$
10		rabeq	$$⊢a=A\to \left\{x\in a|y\in f\left(x\right)\right\}=\left\{x\in A|y\in f\left(x\right)\right\}$$
11	10	adantr	$$⊢\left(a=A\wedge b=B\right)\to \left\{x\in a|y\in f\left(x\right)\right\}=\left\{x\in A|y\in f\left(x\right)\right\}$$
12	9 11	mpteq12dv	$$⊢\left(a=A\wedge b=B\right)\to \left(y\in b⟼\left\{x\in a|y\in f\left(x\right)\right\}\right)=\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\right)$$
13	8 12	mpteq12dv	$$⊢\left(a=A\wedge b=B\right)\to \left(f\in \left({𝒫b}^a\right)⟼\left(y\in b⟼\left\{x\in a|y\in f\left(x\right)\right\}\right)\right)=\left(f\in \left({𝒫B}^A\right)⟼\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\right)\right)$$
14	13	adantl	$$⊢\left(\phi \wedge \left(a=A\wedge b=B\right)\right)\to \left(f\in \left({𝒫b}^a\right)⟼\left(y\in b⟼\left\{x\in a|y\in f\left(x\right)\right\}\right)\right)=\left(f\in \left({𝒫B}^A\right)⟼\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\right)\right)$$
15	2	elexd	$$⊢\phi \to A\in \mathrm{V}$$
16	3	elexd	$$⊢\phi \to B\in \mathrm{V}$$
17		ovex	$$⊢{𝒫B}^A\in \mathrm{V}$$
18	17	mptex	$$⊢\left(f\in \left({𝒫B}^A\right)⟼\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\right)\right)\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to \left(f\in \left({𝒫B}^A\right)⟼\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\right)\right)\in \mathrm{V}$$
20	4 14 15 16 19	ovmpod	$$⊢\phi \to AOB=\left(f\in \left({𝒫B}^A\right)⟼\left(y\in B⟼\left\{x\in A|y\in f\left(x\right)\right\}\right)\right)$$