Metamath Proof Explorer

Theorem elpm2r

Description: Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013)

Ref Expression
Assertion elpm2r 
|- ( ( ( A e. V /\ B e. W ) /\ ( F : C --> A /\ C C_ B ) ) -> F e. ( A ^pm B ) )

Proof

Step Hyp Ref Expression
1 fdm 
 |-  ( F : C --> A -> dom F = C )
2 1 feq2d 
 |-  ( F : C --> A -> ( F : dom F --> A <-> F : C --> A ) )
3 1 sseq1d 
 |-  ( F : C --> A -> ( dom F C_ B <-> C C_ B ) )
4 2 3 anbi12d 
 |-  ( F : C --> A -> ( ( F : dom F --> A /\ dom F C_ B ) <-> ( F : C --> A /\ C C_ B ) ) )
5 4 adantr 
 |-  ( ( F : C --> A /\ C C_ B ) -> ( ( F : dom F --> A /\ dom F C_ B ) <-> ( F : C --> A /\ C C_ B ) ) )
6 5 ibir 
 |-  ( ( F : C --> A /\ C C_ B ) -> ( F : dom F --> A /\ dom F C_ B ) )
7 elpm2g 
 |-  ( ( A e. V /\ B e. W ) -> ( F e. ( A ^pm B ) <-> ( F : dom F --> A /\ dom F C_ B ) ) )
8 6 7 syl5ibr 
 |-  ( ( A e. V /\ B e. W ) -> ( ( F : C --> A /\ C C_ B ) -> F e. ( A ^pm B ) ) )
9 8 imp 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( F : C --> A /\ C C_ B ) ) -> F e. ( A ^pm B ) )