This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } )