Theorem fvrn0

Description: A function value is a member of the range plus null. (Contributed by Scott Fenton, 8-Jun-2011) (Revised by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Assertion	fvrn0	|- ( F ` X ) e. ( ran F u. { (/) } )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( F ` X ) = (/) -> ( F ` X ) = (/) )
2		ssun2	|- { (/) } C_ ( ran F u. { (/) } )
3		0ex	|- (/) e. _V
4	3	snid	|- (/) e. { (/) }
5	2 4	sselii	|- (/) e. ( ran F u. { (/) } )
6	1 5	eqeltrdi	|- ( ( F ` X ) = (/) -> ( F ` X ) e. ( ran F u. { (/) } ) )
7		ssun1	|- ran F C_ ( ran F u. { (/) } )
8		fvprc	|- ( -. X e. _V -> ( F ` X ) = (/) )
9	8	con1i	|- ( -. ( F ` X ) = (/) -> X e. _V )
10		fvexd	|- ( -. ( F ` X ) = (/) -> ( F ` X ) e. _V )
11		fvbr0	|- ( X F ( F ` X ) \/ ( F ` X ) = (/) )
12	11	ori	|- ( -. X F ( F ` X ) -> ( F ` X ) = (/) )
13	12	con1i	|- ( -. ( F ` X ) = (/) -> X F ( F ` X ) )
14		brelrng	|- ( ( X e. _V /\ ( F ` X ) e. _V /\ X F ( F ` X ) ) -> ( F ` X ) e. ran F )
15	9 10 13 14	syl3anc	|- ( -. ( F ` X ) = (/) -> ( F ` X ) e. ran F )
16	7 15	sselid	|- ( -. ( F ` X ) = (/) -> ( F ` X ) e. ( ran F u. { (/) } ) )
17	6 16	pm2.61i	|- ( F ` X ) e. ( ran F u. { (/) } )