Metamath Proof Explorer

Theorem pmsspw

Description: Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion pmsspw 
|- ( A ^pm B ) C_ ~P ( B X. A )

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( f e. ( A ^pm B ) -> -. ( A ^pm B ) = (/) )
2 fnpm 
 |-  ^pm Fn ( _V X. _V )
3 2 fndmi 
 |-  dom ^pm = ( _V X. _V )
4 3 ndmov 
 |-  ( -. ( A e. _V /\ B e. _V ) -> ( A ^pm B ) = (/) )
5 1 4 nsyl2 
 |-  ( f e. ( A ^pm B ) -> ( A e. _V /\ B e. _V ) )
6 elpmg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( f e. ( A ^pm B ) <-> ( Fun f /\ f C_ ( B X. A ) ) ) )
7 5 6 syl 
 |-  ( f e. ( A ^pm B ) -> ( f e. ( A ^pm B ) <-> ( Fun f /\ f C_ ( B X. A ) ) ) )
8 7 ibi 
 |-  ( f e. ( A ^pm B ) -> ( Fun f /\ f C_ ( B X. A ) ) )
9 8 simprd 
 |-  ( f e. ( A ^pm B ) -> f C_ ( B X. A ) )
10 velpw 
 |-  ( f e. ~P ( B X. A ) <-> f C_ ( B X. A ) )
11 9 10 sylibr 
 |-  ( f e. ( A ^pm B ) -> f e. ~P ( B X. A ) )
12 11 ssriv 
 |-  ( A ^pm B ) C_ ~P ( B X. A )