Theorem fsovfvd

Description: Value of the operator, ( A O B ) , which maps between maps from one base set to subsets of the second to maps from the second base set to subsets of the first for base sets, A and B , when applied to function F . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	fsovd.fs	|- O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
	fsovd.a	|- ( ph -> A e. V )
	fsovd.b	|- ( ph -> B e. W )
	fsovfvd.g	|- G = ( A O B )
	fsovfvd.f	|- ( ph -> F e. ( ~P B ^m A ) )
Assertion	fsovfvd	|- ( ph -> ( G ` F ) = ( y e. B |-> { x e. A | y e. ( F ` x ) } ) )

Proof

Step	Hyp	Ref	Expression
1		fsovd.fs	|- O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) )
2		fsovd.a	|- ( ph -> A e. V )
3		fsovd.b	|- ( ph -> B e. W )
4		fsovfvd.g	|- G = ( A O B )
5		fsovfvd.f	|- ( ph -> F e. ( ~P B ^m A ) )
6	1 2 3	fsovd	|- ( ph -> ( A O B ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
7	4 6	syl5eq	|- ( ph -> G = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
8		fveq1	|- ( f = F -> ( f ` x ) = ( F ` x ) )
9	8	eleq2d	|- ( f = F -> ( y e. ( f ` x ) <-> y e. ( F ` x ) ) )
10	9	rabbidv	|- ( f = F -> { x e. A | y e. ( f ` x ) } = { x e. A | y e. ( F ` x ) } )
11	10	mpteq2dv	|- ( f = F -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) = ( y e. B |-> { x e. A | y e. ( F ` x ) } ) )
12	11	adantl	|- ( ( ph /\ f = F ) -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) = ( y e. B |-> { x e. A | y e. ( F ` x ) } ) )
13	3	mptexd	|- ( ph -> ( y e. B |-> { x e. A | y e. ( F ` x ) } ) e. _V )
14	7 12 5 13	fvmptd	|- ( ph -> ( G ` F ) = ( y e. B |-> { x e. A | y e. ( F ` x ) } ) )