Theorem dssmapfv2d

Description: Value of the duality operator for self-mappings of subsets of a base set, B when applied to function F . (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 )
	dssmapfv2d.f	|- ( ph -> F e. ( ~P B ^m ~P B ) )
	dssmapfv2d.g	|- G = ( D ` F )
Assertion	dssmapfv2d	|- ( ph -> G = ( 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		dssmapfv2d.f	|- ( ph -> F e. ( ~P B ^m ~P B ) )
5		dssmapfv2d.g	|- G = ( D ` F )
6	1 2 3	dssmapfvd	|- ( ph -> D = ( f e. ( ~P B ^m ~P B ) |-> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) ) )
7		fveq1	|- ( f = F -> ( f ` ( B \ s ) ) = ( F ` ( B \ s ) ) )
8	7	difeq2d	|- ( f = F -> ( B \ ( f ` ( B \ s ) ) ) = ( B \ ( F ` ( B \ s ) ) ) )
9	8	mpteq2dv	|- ( f = F -> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) = ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) )
10	9	adantl	|- ( ( ph /\ f = F ) -> ( s e. ~P B |-> ( B \ ( f ` ( B \ s ) ) ) ) = ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) )
11		pwexg	|- ( B e. V -> ~P B e. _V )
12		mptexg	|- ( ~P B e. _V -> ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) e. _V )
13	3 11 12	3syl	|- ( ph -> ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) e. _V )
14	6 10 4 13	fvmptd	|- ( ph -> ( D ` F ) = ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) )
15	5 14	syl5eq	|- ( ph -> G = ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) )