Metamath Proof Explorer


Theorem pmvalg

Description: The value of the partial mapping operation. ( A ^pm B ) is the set of all partial functions that map from B to A . (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion pmvalg
|- ( ( A e. C /\ B e. D ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } )

Proof

Step Hyp Ref Expression
1 ssrab2
 |-  { f e. ~P ( B X. A ) | Fun f } C_ ~P ( B X. A )
2 xpexg
 |-  ( ( B e. D /\ A e. C ) -> ( B X. A ) e. _V )
3 2 ancoms
 |-  ( ( A e. C /\ B e. D ) -> ( B X. A ) e. _V )
4 3 pwexd
 |-  ( ( A e. C /\ B e. D ) -> ~P ( B X. A ) e. _V )
5 ssexg
 |-  ( ( { f e. ~P ( B X. A ) | Fun f } C_ ~P ( B X. A ) /\ ~P ( B X. A ) e. _V ) -> { f e. ~P ( B X. A ) | Fun f } e. _V )
6 1 4 5 sylancr
 |-  ( ( A e. C /\ B e. D ) -> { f e. ~P ( B X. A ) | Fun f } e. _V )
7 elex
 |-  ( A e. C -> A e. _V )
8 elex
 |-  ( B e. D -> B e. _V )
9 xpeq2
 |-  ( x = A -> ( y X. x ) = ( y X. A ) )
10 9 pweqd
 |-  ( x = A -> ~P ( y X. x ) = ~P ( y X. A ) )
11 10 rabeqdv
 |-  ( x = A -> { f e. ~P ( y X. x ) | Fun f } = { f e. ~P ( y X. A ) | Fun f } )
12 xpeq1
 |-  ( y = B -> ( y X. A ) = ( B X. A ) )
13 12 pweqd
 |-  ( y = B -> ~P ( y X. A ) = ~P ( B X. A ) )
14 13 rabeqdv
 |-  ( y = B -> { f e. ~P ( y X. A ) | Fun f } = { f e. ~P ( B X. A ) | Fun f } )
15 df-pm
 |-  ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } )
16 11 14 15 ovmpog
 |-  ( ( A e. _V /\ B e. _V /\ { f e. ~P ( B X. A ) | Fun f } e. _V ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } )
17 16 3expia
 |-  ( ( A e. _V /\ B e. _V ) -> ( { f e. ~P ( B X. A ) | Fun f } e. _V -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) )
18 7 8 17 syl2an
 |-  ( ( A e. C /\ B e. D ) -> ( { f e. ~P ( B X. A ) | Fun f } e. _V -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } ) )
19 6 18 mpd
 |-  ( ( A e. C /\ B e. D ) -> ( A ^pm B ) = { f e. ~P ( B X. A ) | Fun f } )