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

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