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

Metamath Proof Explorer

Theorem nfunsn

Description: If the restriction of a class to a singleton is not a function, then its value is the empty set. (An artifact of our function value definition.) (Contributed by NM, 8-Aug-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion nfunsn 
|- ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 eumo 
 |-  ( E! y A F y -> E* y A F y )
2 vex 
 |-  y e. _V
3 2 brresi 
 |-  ( x ( F |` { A } ) y <-> ( x e. { A } /\ x F y ) )
4 velsn 
 |-  ( x e. { A } <-> x = A )
5 breq1 
 |-  ( x = A -> ( x F y <-> A F y ) )
6 4 5 sylbi 
 |-  ( x e. { A } -> ( x F y <-> A F y ) )
7 6 biimpa 
 |-  ( ( x e. { A } /\ x F y ) -> A F y )
8 3 7 sylbi 
 |-  ( x ( F |` { A } ) y -> A F y )
9 8 moimi 
 |-  ( E* y A F y -> E* y x ( F |` { A } ) y )
10 1 9 syl 
 |-  ( E! y A F y -> E* y x ( F |` { A } ) y )
11 tz6.12-2 
 |-  ( -. E! y A F y -> ( F ` A ) = (/) )
12 10 11 nsyl4 
 |-  ( -. ( F ` A ) = (/) -> E* y x ( F |` { A } ) y )
13 12 alrimiv 
 |-  ( -. ( F ` A ) = (/) -> A. x E* y x ( F |` { A } ) y )
14 relres 
 |-  Rel ( F |` { A } )
15 13 14 jctil 
 |-  ( -. ( F ` A ) = (/) -> ( Rel ( F |` { A } ) /\ A. x E* y x ( F |` { A } ) y ) )
16 dffun6 
 |-  ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ A. x E* y x ( F |` { A } ) y ) )
17 15 16 sylibr 
 |-  ( -. ( F ` A ) = (/) -> Fun ( F |` { A } ) )
18 17 con1i 
 |-  ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )