Metamath Proof Explorer

Theorem funssxp

Description: Two ways of specifying a partial function from A to B . (Contributed by NM, 13-Nov-2007)

Ref Expression
Assertion funssxp 
|- ( ( Fun F /\ F C_ ( A X. B ) ) <-> ( F : dom F --> B /\ dom F C_ A ) )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 1 biimpi 
 |-  ( Fun F -> F Fn dom F )
3 rnss 
 |-  ( F C_ ( A X. B ) -> ran F C_ ran ( A X. B ) )
4 rnxpss 
 |-  ran ( A X. B ) C_ B
5 3 4 sstrdi 
 |-  ( F C_ ( A X. B ) -> ran F C_ B )
6 2 5 anim12i 
 |-  ( ( Fun F /\ F C_ ( A X. B ) ) -> ( F Fn dom F /\ ran F C_ B ) )
7 df-f 
 |-  ( F : dom F --> B <-> ( F Fn dom F /\ ran F C_ B ) )
8 6 7 sylibr 
 |-  ( ( Fun F /\ F C_ ( A X. B ) ) -> F : dom F --> B )
9 dmss 
 |-  ( F C_ ( A X. B ) -> dom F C_ dom ( A X. B ) )
10 dmxpss 
 |-  dom ( A X. B ) C_ A
11 9 10 sstrdi 
 |-  ( F C_ ( A X. B ) -> dom F C_ A )
12 11 adantl 
 |-  ( ( Fun F /\ F C_ ( A X. B ) ) -> dom F C_ A )
13 8 12 jca 
 |-  ( ( Fun F /\ F C_ ( A X. B ) ) -> ( F : dom F --> B /\ dom F C_ A ) )
14 ffun 
 |-  ( F : dom F --> B -> Fun F )
15 14 adantr 
 |-  ( ( F : dom F --> B /\ dom F C_ A ) -> Fun F )
16 fssxp 
 |-  ( F : dom F --> B -> F C_ ( dom F X. B ) )
17 xpss1 
 |-  ( dom F C_ A -> ( dom F X. B ) C_ ( A X. B ) )
18 16 17 sylan9ss 
 |-  ( ( F : dom F --> B /\ dom F C_ A ) -> F C_ ( A X. B ) )
19 15 18 jca 
 |-  ( ( F : dom F --> B /\ dom F C_ A ) -> ( Fun F /\ F C_ ( A X. B ) ) )
20 13 19 impbii 
 |-  ( ( Fun F /\ F C_ ( A X. B ) ) <-> ( F : dom F --> B /\ dom F C_ A ) )