Theorem dssmapfv2d

Description: Value of the duality operator for self-mappings of subsets of a base set, B when applied to function F . (Contributed by RP, 19-Apr-2021)

	Ref	Expression
Hypotheses	dssmapfvd.o	$$⊢O=\left(b\in \mathrm{V}⟼\left(f\in \left({𝒫b}^{𝒫b}\right)⟼\left(s\in 𝒫b⟼b\setminus f\left(b\setminus s\right)\right)\right)\right)$$
	dssmapfvd.d	$$⊢D=O\left(B\right)$$
	dssmapfvd.b	$$⊢\phi \to B\in V$$
	dssmapfv2d.f	$$⊢\phi \to F\in \left({𝒫B}^{𝒫B}\right)$$
	dssmapfv2d.g	$$⊢G=D\left(F\right)$$
Assertion	dssmapfv2d	$$⊢\phi \to G=\left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	$$⊢O=\left(b\in \mathrm{V}⟼\left(f\in \left({𝒫b}^{𝒫b}\right)⟼\left(s\in 𝒫b⟼b\setminus f\left(b\setminus s\right)\right)\right)\right)$$
2		dssmapfvd.d	$$⊢D=O\left(B\right)$$
3		dssmapfvd.b	$$⊢\phi \to B\in V$$
4		dssmapfv2d.f	$$⊢\phi \to F\in \left({𝒫B}^{𝒫B}\right)$$
5		dssmapfv2d.g	$$⊢G=D\left(F\right)$$
6	1 2 3	dssmapfvd	$$⊢\phi \to D=\left(f\in \left({𝒫B}^{𝒫B}\right)⟼\left(s\in 𝒫B⟼B\setminus f\left(B\setminus s\right)\right)\right)$$
7		fveq1	$$⊢f=F\to f\left(B\setminus s\right)=F\left(B\setminus s\right)$$
8	7	difeq2d	$$⊢f=F\to B\setminus f\left(B\setminus s\right)=B\setminus F\left(B\setminus s\right)$$
9	8	mpteq2dv	$$⊢f=F\to \left(s\in 𝒫B⟼B\setminus f\left(B\setminus s\right)\right)=\left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)$$
10	9	adantl	$$⊢\left(\phi \wedge f=F\right)\to \left(s\in 𝒫B⟼B\setminus f\left(B\setminus s\right)\right)=\left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)$$
11		pwexg	$$⊢B\in V\to 𝒫B\in \mathrm{V}$$
12		mptexg	$$⊢𝒫B\in \mathrm{V}\to \left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)\in \mathrm{V}$$
13	3 11 12	3syl	$$⊢\phi \to \left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)\in \mathrm{V}$$
14	6 10 4 13	fvmptd	$$⊢\phi \to D\left(F\right)=\left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)$$
15	5 14	eqtrid	$$⊢\phi \to G=\left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)$$