This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffnfv

Description: A function maps to a class to which all values belong. (Contributed by NM, 3-Dec-2003)

Ref Expression
Assertion ffnfv 
|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 ffvelcdm 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
3 2 ralrimiva 
 |-  ( F : A --> B -> A. x e. A ( F ` x ) e. B )
4 1 3 jca 
 |-  ( F : A --> B -> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5 simpl 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F Fn A )
6 fvelrnb 
 |-  ( F Fn A -> ( y e. ran F <-> E. x e. A ( F ` x ) = y ) )
7 6 biimpd 
 |-  ( F Fn A -> ( y e. ran F -> E. x e. A ( F ` x ) = y ) )
8 nfra1 
 |-  F/ x A. x e. A ( F ` x ) e. B
9 nfv 
 |-  F/ x y e. B
10 rsp 
 |-  ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( F ` x ) e. B ) )
11 eleq1 
 |-  ( ( F ` x ) = y -> ( ( F ` x ) e. B <-> y e. B ) )
12 11 biimpcd 
 |-  ( ( F ` x ) e. B -> ( ( F ` x ) = y -> y e. B ) )
13 10 12 syl6 
 |-  ( A. x e. A ( F ` x ) e. B -> ( x e. A -> ( ( F ` x ) = y -> y e. B ) ) )
14 8 9 13 rexlimd 
 |-  ( A. x e. A ( F ` x ) e. B -> ( E. x e. A ( F ` x ) = y -> y e. B ) )
15 7 14 sylan9 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( y e. ran F -> y e. B ) )
16 15 ssrdv 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )
17 df-f 
 |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
18 5 16 17 sylanbrc 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> B )
19 4 18 impbii 
 |-  ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )