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 = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
	dssmapfvd.d	|- D = ( O ` B )
	dssmapfvd.b	|- ( ph -> B e. V )
Assertion	dssmap2d	|- ( ph -> ( D o. D ) = ( _I |` ( ~P B ^m ~P B ) ) )

Proof

Step	Hyp	Ref	Expression
1		dssmapfvd.o	|- O = ( b e. _V |-> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) )
2		dssmapfvd.d	|- D = ( O ` B )
3		dssmapfvd.b	|- ( ph -> B e. V )
4	1 2 3	dssmapnvod	|- ( ph -> `' D = D )
5	4	coeq1d	|- ( ph -> ( `' D o. D ) = ( D o. D ) )
6	1 2 3	dssmapf1od	|- ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
7		f1ococnv1	|- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> ( `' D o. D ) = ( _I |` ( ~P B ^m ~P B ) ) )
8	6 7	syl	|- ( ph -> ( `' D o. D ) = ( _I |` ( ~P B ^m ~P B ) ) )
9	5 8	eqtr3d	|- ( ph -> ( D o. D ) = ( _I |` ( ~P B ^m ~P B ) ) )