Theorem dssmap2d

Description: For any base set B the duality operator for self-mappings of subsets of that base set when composed with itself is the restricted identity operator. (Contributed by RP, 21-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$$
Assertion	dssmap2d	$$⊢\phi \to D\circ D={\mathrm{I}\upharpoonright }_{\left({𝒫B}^{𝒫B}\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	1 2 3	dssmapnvod	$$⊢\phi \to D^{-1}=D$$
5	4	coeq1d	$$⊢\phi \to D^{-1}\circ D=D\circ D$$
6	1 2 3	dssmapf1od	$$⊢\phi \to D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}$$
7		f1ococnv1	$$⊢D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}\to D^{-1}\circ D={\mathrm{I}\upharpoonright }_{\left({𝒫B}^{𝒫B}\right)}$$
8	6 7	syl	$$⊢\phi \to D^{-1}\circ D={\mathrm{I}\upharpoonright }_{\left({𝒫B}^{𝒫B}\right)}$$
9	5 8	eqtr3d	$$⊢\phi \to D\circ D={\mathrm{I}\upharpoonright }_{\left({𝒫B}^{𝒫B}\right)}$$