Metamath Proof Explorer


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