Theorem elpmg

Description: The predicate "is a partial function". (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Assertion	elpmg	|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmvalg	|- ( ( A e. V /\ B e. W ) -> ( A ^pm B ) = { g e. ~P ( B X. A ) | Fun g } )
2	1	eleq2d	|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> C e. { g e. ~P ( B X. A ) | Fun g } ) )
3		funeq	|- ( g = C -> ( Fun g <-> Fun C ) )
4	3	elrab	|- ( C e. { g e. ~P ( B X. A ) | Fun g } <-> ( C e. ~P ( B X. A ) /\ Fun C ) )
5	2 4	bitrdi	|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( C e. ~P ( B X. A ) /\ Fun C ) ) )
6	5	biancomd	|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C e. ~P ( B X. A ) ) ) )
7		elex	|- ( C e. ~P ( B X. A ) -> C e. _V )
8	7	a1i	|- ( ( A e. V /\ B e. W ) -> ( C e. ~P ( B X. A ) -> C e. _V ) )
9		xpexg	|- ( ( B e. W /\ A e. V ) -> ( B X. A ) e. _V )
10	9	ancoms	|- ( ( A e. V /\ B e. W ) -> ( B X. A ) e. _V )
11		ssexg	|- ( ( C C_ ( B X. A ) /\ ( B X. A ) e. _V ) -> C e. _V )
12	11	expcom	|- ( ( B X. A ) e. _V -> ( C C_ ( B X. A ) -> C e. _V ) )
13	10 12	syl	|- ( ( A e. V /\ B e. W ) -> ( C C_ ( B X. A ) -> C e. _V ) )
14		elpwg	|- ( C e. _V -> ( C e. ~P ( B X. A ) <-> C C_ ( B X. A ) ) )
15	14	a1i	|- ( ( A e. V /\ B e. W ) -> ( C e. _V -> ( C e. ~P ( B X. A ) <-> C C_ ( B X. A ) ) ) )
16	8 13 15	pm5.21ndd	|- ( ( A e. V /\ B e. W ) -> ( C e. ~P ( B X. A ) <-> C C_ ( B X. A ) ) )
17	16	anbi2d	|- ( ( A e. V /\ B e. W ) -> ( ( Fun C /\ C e. ~P ( B X. A ) ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) )
18	6 17	bitrd	|- ( ( A e. V /\ B e. W ) -> ( C e. ( A ^pm B ) <-> ( Fun C /\ C C_ ( B X. A ) ) ) )