Theorem dssmapfv3d

Description: Value of the duality operator for self-mappings of subsets of a base set, B when applied to function F and subset S . (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)$$
	dssmapfv3d.s	$$⊢\phi \to S\in 𝒫B$$
	dssmapfv3d.t	$$⊢T=G\left(S\right)$$
Assertion	dssmapfv3d	$$⊢\phi \to T=B\setminus F\left(B\setminus S\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		dssmapfv3d.s	$$⊢\phi \to S\in 𝒫B$$
7		dssmapfv3d.t	$$⊢T=G\left(S\right)$$
8	1 2 3 4 5	dssmapfv2d	$$⊢\phi \to G=\left(s\in 𝒫B⟼B\setminus F\left(B\setminus s\right)\right)$$
9		difeq2	$$⊢s=S\to B\setminus s=B\setminus S$$
10	9	fveq2d	$$⊢s=S\to F\left(B\setminus s\right)=F\left(B\setminus S\right)$$
11	10	difeq2d	$$⊢s=S\to B\setminus F\left(B\setminus s\right)=B\setminus F\left(B\setminus S\right)$$
12	11	adantl	$$⊢\left(\phi \wedge s=S\right)\to B\setminus F\left(B\setminus s\right)=B\setminus F\left(B\setminus S\right)$$
13	3	difexd	$$⊢\phi \to B\setminus F\left(B\setminus S\right)\in \mathrm{V}$$
14	8 12 6 13	fvmptd	$$⊢\phi \to G\left(S\right)=B\setminus F\left(B\setminus S\right)$$
15	7 14	syl5eq	$$⊢\phi \to T=B\setminus F\left(B\setminus S\right)$$