Theorem fsovfvfvd

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 and element Y . (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 ) )
	fsovfvfvd.h	|- H = ( G ` F )
	fsovfvfvd.y	|- ( ph -> Y e. B )
Assertion	fsovfvfvd	|- ( ph -> ( H ` Y ) = { 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		fsovfvfvd.h	|- H = ( G ` F )
7		fsovfvfvd.y	|- ( ph -> Y e. B )
8	1 2 3 4 5	fsovfvd	|- ( ph -> ( G ` F ) = ( y e. B |-> { x e. A | y e. ( F ` x ) } ) )
9	6 8	syl5eq	|- ( ph -> H = ( y e. B |-> { x e. A | y e. ( F ` x ) } ) )
10		eleq1	|- ( y = Y -> ( y e. ( F ` x ) <-> Y e. ( F ` x ) ) )
11	10	rabbidv	|- ( y = Y -> { x e. A | y e. ( F ` x ) } = { x e. A | Y e. ( F ` x ) } )
12	11	adantl	|- ( ( ph /\ y = Y ) -> { x e. A | y e. ( F ` x ) } = { x e. A | Y e. ( F ` x ) } )
13		rabexg	|- ( A e. V -> { x e. A | Y e. ( F ` x ) } e. _V )
14	2 13	syl	|- ( ph -> { x e. A | Y e. ( F ` x ) } e. _V )
15	9 12 7 14	fvmptd	|- ( ph -> ( H ` Y ) = { x e. A | Y e. ( F ` x ) } )