Metamath Proof Explorer

Theorem ffvresb

Description: A necessary and sufficient condition for a restricted function. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion ffvresb 
|- ( Fun F -> ( ( F |` A ) : A --> B <-> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) )

Proof

Step Hyp Ref Expression
1 fdm 
 |-  ( ( F |` A ) : A --> B -> dom ( F |` A ) = A )
2 dmres 
 |-  dom ( F |` A ) = ( A i^i dom F )
3 inss2 
 |-  ( A i^i dom F ) C_ dom F
4 2 3 eqsstri 
 |-  dom ( F |` A ) C_ dom F
5 1 4 eqsstrrdi 
 |-  ( ( F |` A ) : A --> B -> A C_ dom F )
6 5 sselda 
 |-  ( ( ( F |` A ) : A --> B /\ x e. A ) -> x e. dom F )
7 fvres 
 |-  ( x e. A -> ( ( F |` A ) ` x ) = ( F ` x ) )
8 7 adantl 
 |-  ( ( ( F |` A ) : A --> B /\ x e. A ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
9 ffvelcdm 
 |-  ( ( ( F |` A ) : A --> B /\ x e. A ) -> ( ( F |` A ) ` x ) e. B )
10 8 9 eqeltrrd 
 |-  ( ( ( F |` A ) : A --> B /\ x e. A ) -> ( F ` x ) e. B )
11 6 10 jca 
 |-  ( ( ( F |` A ) : A --> B /\ x e. A ) -> ( x e. dom F /\ ( F ` x ) e. B ) )
12 11 ralrimiva 
 |-  ( ( F |` A ) : A --> B -> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) )
13 simpl 
 |-  ( ( x e. dom F /\ ( F ` x ) e. B ) -> x e. dom F )
14 13 ralimi 
 |-  ( A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) -> A. x e. A x e. dom F )
15 dfss3 
 |-  ( A C_ dom F <-> A. x e. A x e. dom F )
16 14 15 sylibr 
 |-  ( A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) -> A C_ dom F )
17 funfn 
 |-  ( Fun F <-> F Fn dom F )
18 fnssres 
 |-  ( ( F Fn dom F /\ A C_ dom F ) -> ( F |` A ) Fn A )
19 17 18 sylanb 
 |-  ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) Fn A )
20 16 19 sylan2 
 |-  ( ( Fun F /\ A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) -> ( F |` A ) Fn A )
21 simpr 
 |-  ( ( x e. dom F /\ ( F ` x ) e. B ) -> ( F ` x ) e. B )
22 7 eleq1d 
 |-  ( x e. A -> ( ( ( F |` A ) ` x ) e. B <-> ( F ` x ) e. B ) )
23 21 22 imbitrrid 
 |-  ( x e. A -> ( ( x e. dom F /\ ( F ` x ) e. B ) -> ( ( F |` A ) ` x ) e. B ) )
24 23 ralimia 
 |-  ( A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) -> A. x e. A ( ( F |` A ) ` x ) e. B )
25 24 adantl 
 |-  ( ( Fun F /\ A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) -> A. x e. A ( ( F |` A ) ` x ) e. B )
26 fnfvrnss 
 |-  ( ( ( F |` A ) Fn A /\ A. x e. A ( ( F |` A ) ` x ) e. B ) -> ran ( F |` A ) C_ B )
27 20 25 26 syl2anc 
 |-  ( ( Fun F /\ A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) -> ran ( F |` A ) C_ B )
28 df-f 
 |-  ( ( F |` A ) : A --> B <-> ( ( F |` A ) Fn A /\ ran ( F |` A ) C_ B ) )
29 20 27 28 sylanbrc 
 |-  ( ( Fun F /\ A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) -> ( F |` A ) : A --> B )
30 29 ex 
 |-  ( Fun F -> ( A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) -> ( F |` A ) : A --> B ) )
31 12 30 impbid2 
 |-  ( Fun F -> ( ( F |` A ) : A --> B <-> A. x e. A ( x e. dom F /\ ( F ` x ) e. B ) ) )