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 ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eumo	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃* 𝑦 𝐴 𝐹 𝑦 )
2		vex	⊢ 𝑦 ∈ V
3	2	brresi	⊢ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) )
4		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
5		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
6	4 5	sylbi	⊢ ( 𝑥 ∈ { 𝐴 } → ( 𝑥 𝐹 𝑦 ↔ 𝐴 𝐹 𝑦 ) )
7	6	biimpa	⊢ ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑥 𝐹 𝑦 ) → 𝐴 𝐹 𝑦 )
8	3 7	sylbi	⊢ ( 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 → 𝐴 𝐹 𝑦 )
9	8	moimi	⊢ ( ∃* 𝑦 𝐴 𝐹 𝑦 → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
10	1 9	syl	⊢ ( ∃! 𝑦 𝐴 𝐹 𝑦 → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
11		tz6.12-2	⊢ ( ¬ ∃! 𝑦 𝐴 𝐹 𝑦 → ( 𝐹 ‘ 𝐴 ) = ∅ )
12	10 11	nsyl4	⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
13	12	alrimiv	⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 )
14		relres	⊢ Rel ( 𝐹 ↾ { 𝐴 } )
15	13 14	jctil	⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
16		dffun6	⊢ ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ ( Rel ( 𝐹 ↾ { 𝐴 } ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ { 𝐴 } ) 𝑦 ) )
17	15 16	sylibr	⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → Fun ( 𝐹 ↾ { 𝐴 } ) )
18	17	con1i	⊢ ( ¬ Fun ( 𝐹 ↾ { 𝐴 } ) → ( 𝐹 ‘ 𝐴 ) = ∅ )