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

Metamath Proof Explorer

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. { (/) } )