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