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=bVf𝒫b𝒫bs𝒫bbfbs
dssmapfvd.d D=OB
dssmapfvd.b φBV
dssmapfv2d.f φF𝒫B𝒫B
dssmapfv2d.g G=DF
dssmapfv3d.s φS𝒫B
dssmapfv3d.t T=GS
Assertion dssmapfv3d φT=BFBS

Proof

Step Hyp Ref Expression
1 dssmapfvd.o O=bVf𝒫b𝒫bs𝒫bbfbs
2 dssmapfvd.d D=OB
3 dssmapfvd.b φBV
4 dssmapfv2d.f φF𝒫B𝒫B
5 dssmapfv2d.g G=DF
6 dssmapfv3d.s φS𝒫B
7 dssmapfv3d.t T=GS
8 1 2 3 4 5 dssmapfv2d φG=s𝒫BBFBs
9 difeq2 s=SBs=BS
10 9 fveq2d s=SFBs=FBS
11 10 difeq2d s=SBFBs=BFBS
12 11 adantl φs=SBFBs=BFBS
13 3 difexd φBFBSV
14 8 12 6 13 fvmptd φGS=BFBS
15 7 14 eqtrid φT=BFBS