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

Metamath Proof Explorer

Theorem chfnrn

Description: The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain. (Contributed by NM, 31-Aug-1999)

Ref Expression
Assertion chfnrn 
|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. x ) -> ran F C_ U. A )

Proof

Step Hyp Ref Expression
1 fvelrnb 
 |-  ( F Fn A -> ( y e. ran F <-> E. x e. A ( F ` x ) = y ) )
2 1 biimpd 
 |-  ( F Fn A -> ( y e. ran F -> E. x e. A ( F ` x ) = y ) )
3 eleq1 
 |-  ( ( F ` x ) = y -> ( ( F ` x ) e. x <-> y e. x ) )
4 3 biimpcd 
 |-  ( ( F ` x ) e. x -> ( ( F ` x ) = y -> y e. x ) )
5 4 ralimi 
 |-  ( A. x e. A ( F ` x ) e. x -> A. x e. A ( ( F ` x ) = y -> y e. x ) )
6 rexim 
 |-  ( A. x e. A ( ( F ` x ) = y -> y e. x ) -> ( E. x e. A ( F ` x ) = y -> E. x e. A y e. x ) )
7 5 6 syl 
 |-  ( A. x e. A ( F ` x ) e. x -> ( E. x e. A ( F ` x ) = y -> E. x e. A y e. x ) )
8 2 7 sylan9 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. x ) -> ( y e. ran F -> E. x e. A y e. x ) )
9 eluni2 
 |-  ( y e. U. A <-> E. x e. A y e. x )
10 8 9 imbitrrdi 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. x ) -> ( y e. ran F -> y e. U. A ) )
11 10 ssrdv 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. x ) -> ran F C_ U. A )