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 )