# Metamath Proof Explorer

## 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 difexg ${⊢}{B}\in {V}\to {B}\setminus {F}\left({B}\setminus {S}\right)\in \mathrm{V}$
14 3 13 syl ${⊢}{\phi }\to {B}\setminus {F}\left({B}\setminus {S}\right)\in \mathrm{V}$
15 8 12 6 14 fvmptd ${⊢}{\phi }\to {G}\left({S}\right)={B}\setminus {F}\left({B}\setminus {S}\right)$
16 7 15 syl5eq ${⊢}{\phi }\to {T}={B}\setminus {F}\left({B}\setminus {S}\right)$