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 = ( 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 )
	dssmapfv3d.s	|- ( ph -> S e. ~P B )
	dssmapfv3d.t	|- T = ( G ` S )
Assertion	dssmapfv3d	|- ( ph -> T = ( 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		dssmapfv3d.s	|- ( ph -> S e. ~P B )
7		dssmapfv3d.t	|- T = ( G ` S )
8	1 2 3 4 5	dssmapfv2d	|- ( ph -> G = ( s e. ~P B |-> ( B \ ( F ` ( B \ s ) ) ) ) )
9		difeq2	|- ( s = S -> ( B \ s ) = ( B \ S ) )
10	9	fveq2d	|- ( s = S -> ( F ` ( B \ s ) ) = ( F ` ( B \ S ) ) )
11	10	difeq2d	|- ( s = S -> ( B \ ( F ` ( B \ s ) ) ) = ( B \ ( F ` ( B \ S ) ) ) )
12	11	adantl	|- ( ( ph /\ s = S ) -> ( B \ ( F ` ( B \ s ) ) ) = ( B \ ( F ` ( B \ S ) ) ) )
13		difexg	|- ( B e. V -> ( B \ ( F ` ( B \ S ) ) ) e. _V )
14	3 13	syl	|- ( ph -> ( B \ ( F ` ( B \ S ) ) ) e. _V )
15	8 12 6 14	fvmptd	|- ( ph -> ( G ` S ) = ( B \ ( F ` ( B \ S ) ) ) )
16	7 15	syl5eq	|- ( ph -> T = ( B \ ( F ` ( B \ S ) ) ) )