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 ) = (/) )