Theorem fsovfd

Description: 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 , gives a function between two sets of functions. (Contributed by RP, 27-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 )
Assertion	fsovfd	|- ( ph -> G : ( ~P B ^m A ) --> ( ~P A ^m B ) )

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	1 2 3	fsovd	|- ( ph -> ( A O B ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
6	4 5	eqtrid	|- ( ph -> G = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
7		ssrab2	|- { x e. A | y e. ( f ` x ) } C_ A
8	7	a1i	|- ( ph -> { x e. A | y e. ( f ` x ) } C_ A )
9	2 8	sselpwd	|- ( ph -> { x e. A | y e. ( f ` x ) } e. ~P A )
10	9	adantr	|- ( ( ph /\ y e. B ) -> { x e. A | y e. ( f ` x ) } e. ~P A )
11	10	fmpttd	|- ( ph -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) : B --> ~P A )
12	2	pwexd	|- ( ph -> ~P A e. _V )
13	12 3	elmapd	|- ( ph -> ( ( y e. B |-> { x e. A | y e. ( f ` x ) } ) e. ( ~P A ^m B ) <-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) : B --> ~P A ) )
14	11 13	mpbird	|- ( ph -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) e. ( ~P A ^m B ) )
15	14	adantr	|- ( ( ph /\ f e. ( ~P B ^m A ) ) -> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) e. ( ~P A ^m B ) )
16	6 15	fmpt3d	|- ( ph -> G : ( ~P B ^m A ) --> ( ~P A ^m B ) )