Theorem fvclss

Description: Upper bound for the class of values of a class. (Contributed by NM, 9-Nov-1995)

	Ref	Expression
Assertion	fvclss	|- { y | E. x y = ( F ` x ) } C_ ( ran F u. { (/) } )

Proof

Step	Hyp	Ref	Expression
1		eqcom	|- ( y = ( F ` x ) <-> ( F ` x ) = y )
2		tz6.12i	|- ( y =/= (/) -> ( ( F ` x ) = y -> x F y ) )
3	1 2	biimtrid	|- ( y =/= (/) -> ( y = ( F ` x ) -> x F y ) )
4	3	eximdv	|- ( y =/= (/) -> ( E. x y = ( F ` x ) -> E. x x F y ) )
5		vex	|- y e. _V
6	5	elrn	|- ( y e. ran F <-> E. x x F y )
7	4 6	imbitrrdi	|- ( y =/= (/) -> ( E. x y = ( F ` x ) -> y e. ran F ) )
8	7	com12	|- ( E. x y = ( F ` x ) -> ( y =/= (/) -> y e. ran F ) )
9	8	necon1bd	|- ( E. x y = ( F ` x ) -> ( -. y e. ran F -> y = (/) ) )
10		velsn	|- ( y e. { (/) } <-> y = (/) )
11	9 10	imbitrrdi	|- ( E. x y = ( F ` x ) -> ( -. y e. ran F -> y e. { (/) } ) )
12	11	orrd	|- ( E. x y = ( F ` x ) -> ( y e. ran F \/ y e. { (/) } ) )
13	12	ss2abi	|- { y | E. x y = ( F ` x ) } C_ { y | ( y e. ran F \/ y e. { (/) } ) }
14		df-un	|- ( ran F u. { (/) } ) = { y | ( y e. ran F \/ y e. { (/) } ) }
15	13 14	sseqtrri	|- { y | E. x y = ( F ` x ) } C_ ( ran F u. { (/) } )