Theorem fvssunirn

Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	fvssunirn	|- ( F ` X ) C_ U. ran F

Proof

Step	Hyp	Ref	Expression
1		fvrn0	|- ( F ` X ) e. ( ran F u. { (/) } )
2		elssuni	|- ( ( F ` X ) e. ( ran F u. { (/) } ) -> ( F ` X ) C_ U. ( ran F u. { (/) } ) )
3	1 2	ax-mp	|- ( F ` X ) C_ U. ( ran F u. { (/) } )
4		uniun	|- U. ( ran F u. { (/) } ) = ( U. ran F u. U. { (/) } )
5		0ex	|- (/) e. _V
6	5	unisn	|- U. { (/) } = (/)
7	6	uneq2i	|- ( U. ran F u. U. { (/) } ) = ( U. ran F u. (/) )
8		un0	|- ( U. ran F u. (/) ) = U. ran F
9	4 7 8	3eqtri	|- U. ( ran F u. { (/) } ) = U. ran F
10	3 9	sseqtri	|- ( F ` X ) C_ U. ran F