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

Metamath Proof Explorer

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