Theorem dssmapfvd

Description: Value of the duality operator for self-mappings of subsets of a base set, B . (Contributed by RP, 19-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	dssmapfvd	|- ( ph -> D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )

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		pweq	|- ( b = B -> ~P b = ~P B )
5	4 4	oveq12d	|- ( b = B -> ( ~P b ^m ~P b ) = ( ~P B ^m ~P B ) )
6		id	|- ( b = B -> b = B )
7		difeq1	|- ( b = B -> ( b \ s ) = ( B \ s ) )
8	7	fveq2d	|- ( b = B -> ( f ` ( b \ s ) ) = ( f ` ( B \ s ) ) )
9	6 8	difeq12d	|- ( b = B -> ( b \ ( f ` ( b \ s ) ) ) = ( B \ ( f ` ( B \ s ) ) ) )
10	4 9	mpteq12dv	|- ( b = B -> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) = ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) )
11	5 10	mpteq12dv	|- ( b = B -> ( f e. ( ~P b ^m ~P b ) |-> ( s e. ~P b |-> ( b \ ( f ` ( b \ s ) ) ) ) ) = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
12	3	elexd	|- ( ph -> B e. _V )
13		ovex	|- ( ~P B ^m ~P B ) e. _V
14		mptexg	|- ( ( ~P B ^m ~P B ) e. _V -> ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) e. _V )
15	13 14	mp1i	|- ( ph -> ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) e. _V )
16	1 11 12 15	fvmptd3	|- ( ph -> ( O ` B ) = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
17	2 16	syl5eq	|- ( ph -> D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )