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 ⊢ ∃! y A F y → ∃* y A F y
2 vex ⊢ y ∈ V
3 2 brresi ⊢ x F ↾ A y ↔ x ∈ A ∧ x F y
4 velsn ⊢ x ∈ A ↔ x = A
5 breq1 ⊢ x = A → x F y ↔ A F y
6 4 5 sylbi ⊢ x ∈ A → x F y ↔ A F y
7 6 biimpa ⊢ x ∈ A ∧ x F y → A F y
8 3 7 sylbi ⊢ x F ↾ A y → A F y
9 8 moimi ⊢ ∃* y A F y → ∃* y x F ↾ A y
10 1 9 syl ⊢ ∃! y A F y → ∃* y x F ↾ A y
11 tz6.12-2 ⊢ ¬ ∃! y A F y → F ⁡ A = ∅
12 10 11 nsyl4 ⊢ ¬ F ⁡ A = ∅ → ∃* y x F ↾ A y
13 12 alrimiv ⊢ ¬ F ⁡ A = ∅ → ∀ x ∃* y x F ↾ A y
14 relres ⊢ Rel ⁡ F ↾ A
15 13 14 jctil ⊢ ¬ F ⁡ A = ∅ → Rel ⁡ F ↾ A ∧ ∀ x ∃* y x F ↾ A y
16 dffun6 ⊢ Fun ⁡ F ↾ A ↔ Rel ⁡ F ↾ A ∧ ∀ x ∃* y x F ↾ A y
17 15 16 sylibr ⊢ ¬ F ⁡ A = ∅ → Fun ⁡ F ↾ A
18 17 con1i ⊢ ¬ Fun ⁡ F ↾ A → F ⁡ A = ∅