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 )