Metamath Proof Explorer

Theorem fsovd

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 . (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 )
Assertion fsovd 
|- ( ph -> ( A O B ) = ( f e. ( ~P B ^m A ) |-> ( 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 1 a1i 
 |-  ( ph -> O = ( a e. _V , b e. _V |-> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) ) )
5 pweq 
 |-  ( b = B -> ~P b = ~P B )
6 5 adantl 
 |-  ( ( a = A /\ b = B ) -> ~P b = ~P B )
7 simpl 
 |-  ( ( a = A /\ b = B ) -> a = A )
8 6 7 oveq12d 
 |-  ( ( a = A /\ b = B ) -> ( ~P b ^m a ) = ( ~P B ^m A ) )
9 simpr 
 |-  ( ( a = A /\ b = B ) -> b = B )
10 rabeq 
 |-  ( a = A -> { x e. a | y e. ( f ` x ) } = { x e. A | y e. ( f ` x ) } )
11 10 adantr 
 |-  ( ( a = A /\ b = B ) -> { x e. a | y e. ( f ` x ) } = { x e. A | y e. ( f ` x ) } )
12 9 11 mpteq12dv 
 |-  ( ( a = A /\ b = B ) -> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) = ( y e. B |-> { x e. A | y e. ( f ` x ) } ) )
13 8 12 mpteq12dv 
 |-  ( ( a = A /\ b = B ) -> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
14 13 adantl 
 |-  ( ( ph /\ ( a = A /\ b = B ) ) -> ( f e. ( ~P b ^m a ) |-> ( y e. b |-> { x e. a | y e. ( f ` x ) } ) ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )
15 2 elexd 
 |-  ( ph -> A e. _V )
16 3 elexd 
 |-  ( ph -> B e. _V )
17 ovex 
 |-  ( ~P B ^m A ) e. _V
18 17 mptex 
 |-  ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) e. _V
19 18 a1i 
 |-  ( ph -> ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) e. _V )
20 4 14 15 16 19 ovmpod 
 |-  ( ph -> ( A O B ) = ( f e. ( ~P B ^m A ) |-> ( y e. B |-> { x e. A | y e. ( f ` x ) } ) ) )